MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breq1 Structured version   GIF version

Theorem breq1 4246
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))

Proof of Theorem breq1
StepHypRef Expression
1 opeq1 4013 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21eleq1d 2509 . 2 (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3 df-br 4244 . 2 (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4 df-br 4244 . 2 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
52, 3, 43bitr4g 281 1 (𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 178   = wceq 1654  wcel 1728  cop 3846   class class class wbr 4243
This theorem is referenced by:  breq12  4248  breq1i  4250  breq1d  4253  nbrne2  4261  brab1  4288  pocl  4545  swopolem  4547  swopo  4548  solin  4561  sotrieq  4565  sotr2  4567  isso2i  4570  somo  4572  frirr  4594  fr2nr  4595  wereu2  4614  fr3nr  4795  dfwe2  4797  vtoclr  4957  frsn  4983  brcog  5074  brcogw  5076  opelcnvg  5087  dfdmf  5099  eldmg  5100  dfrnf  5143  dfres2  5228  imasng  5261  asymref2  5286  sotri2  5298  somin1  5305  coi1  5420  dffun6f  5503  funmo  5505  fun11  5551  fveq2  5763  nfunsn  5792  dffv2  5832  dff3  5918  f1ompt  5927  fmptco  5937  dff13  6040  foeqcnvco  6063  isorel  6082  soisores  6083  soisoi  6084  isocnv  6086  isotr  6092  isomin  6093  isoini  6094  isopolem  6101  isosolem  6103  f1oiso  6107  f1oiso2  6108  f1oweALT  6110  weniso  6111  caovordig  6288  caovordg  6290  caovord3d  6293  caovord  6294  caovord3  6296  caofrss  6373  caoftrn  6375  frxp  6492  poxp  6494  fnse  6499  brtpos2  6521  rntpos  6528  tpostpos  6535  fvopab5  6570  ertr  6956  ecopovsym  7042  ecopovtrn  7043  th3qlem2  7047  isfi  7167  en0  7206  en1  7210  endisj  7231  xpcomco  7234  sbth  7263  2pwne  7299  disjenex  7301  ssenen  7317  nneneq  7326  php  7327  sdom1  7344  isinf  7358  fineqvlem  7359  pssnn  7363  enp1i  7379  findcard  7383  findcard2  7384  findcard3  7386  frfi  7388  fiint  7419  marypha1lem  7474  supmo  7493  eqsup  7497  supub  7500  suplub  7501  supmaxlem  7505  suppr  7509  supisolem  7511  supisoex  7512  ordtypecbv  7522  ordtypelem3  7525  ordtypelem6  7528  ordtypelem7  7529  ordtypelem9  7531  ordtypelem10  7532  hartogslem1  7547  hartogs  7549  wemaplem1  7551  wemaplem2  7552  card2on  7558  card2inf  7559  elharval  7567  brwdom2  7577  wdomtr  7579  cantnfp1lem2  7671  cantnflem1  7681  wemapwe  7690  r111  7737  kardex  7856  karden  7857  isnumi  7871  tskwe  7875  cardid2  7878  cardonle  7882  cardne  7890  iscard2  7901  infxpenlem  7933  fodomfi2  7979  wdomfil  7980  wdomnumr  7983  alephsuc2  7999  infenaleph  8010  iunfictbso  8033  infpss  8135  cff1  8176  cfslb2n  8186  sornom  8195  fin4i  8216  isfin6  8218  isfin7  8219  isfin1-3  8304  fin1a2lem9  8326  fin1a2lem11  8328  hsmexlem4  8347  axcc2lem  8354  axcc4dom  8359  domtriomlem  8360  numthcor  8412  zorn2lem2  8415  zorn2lem3  8416  zorn2lem7  8420  zorn2g  8421  axdclem  8437  axdc  8439  brdom7disj  8447  brdom6disj  8448  uniimadom  8457  ondomon  8476  alephval2  8485  alephreg  8495  pwcfsdom  8496  elgch  8535  gchi  8537  fpwwe2lem12  8554  fpwwe2lem13  8555  pwfseqlem4  8575  winainflem  8606  winalim2  8609  tsken  8667  0tsk  8668  inar1  8688  tskord  8693  tskuni  8696  grudomon  8730  pinq  8842  nqereu  8844  enqeq  8849  ltbtwnnq  8893  ltrnq  8894  prcdnq  8908  prnmax  8910  genpnmax  8922  nqpr  8929  1idpr  8944  reclem2pr  8963  reclem3pr  8964  reclem4pr  8965  recexpr  8966  supexpr  8969  ltsosr  9007  1ne0sr  9009  ltasr  9013  supsrlem  9024  axpre-lttri  9078  axpre-lttrn  9079  axpre-ltadd  9080  axpre-sup  9082  lelttr  9203  ltordlem  9590  lt0ne0d  9630  fimaxre3  9995  lbreu  9996  lble  9998  sup2  10002  infm3  10005  suprleub  10010  supmul1  10011  supmullem1  10012  supmul  10014  nnsub  10076  nominpos  10242  nnunb  10255  arch  10256  nn0sub  10308  nn0n0n1ge2b  10319  zextle  10381  peano5uzti  10397  fzind  10406  btwnz  10410  uzval  10528  uzwo  10577  uzwoOLD  10578  nnwof  10581  uzinfmi  10593  ublbneg  10598  lbzbi  10602  zsupss  10603  uzsupss  10606  uzwo3  10607  zmax  10609  rebtwnz  10611  rpnnen1lem3  10640  xrltnsym  10768  xrlttri  10770  xrlttr  10771  xrlelttr  10784  nltpnft  10792  xrmaxlt  10807  xrmaxle  10809  qbtwnre  10823  qbtwnxr  10824  xltnegi  10840  xsubge0  10878  xlesubadd  10880  xmullem2  10882  xlemul1a  10905  xrinfmexpnf  10922  xrsupsslem  10923  xrinfmsslem  10924  xrub  10928  supxrunb1  10936  supxrunb2  10937  ixxval  10962  elixx1  10963  elioo2  10995  iccid  10999  icc0  11002  fzval  11083  elfz1  11086  elfznelfzo  11230  elfznelfzob  11231  flval  11241  fllelt  11244  flval2  11259  flval3  11260  flbi  11261  modid2  11309  fsequb2  11353  seqf1olem2  11401  sqlecan  11525  faclbnd4lem1  11622  sqrlem6  12091  01sqrex  12093  abslt  12156  absle  12157  rexanre  12188  rexico  12195  limsupgle  12309  limsupgre  12313  limsupbnd2  12315  rlim2lt  12329  rlim3  12330  ello12r  12349  ello1d  12355  elo12r  12360  rlimconst  12376  climshft  12408  rlimcn2  12422  o1rlimmul  12450  lo1le  12483  climsup  12501  caucvgrlem  12504  isumless  12663  divrcnv  12670  cvgrat  12698  rpnnen2lem10  12861  ruclem1  12868  ruclem2  12869  ruclem11  12877  ruclem12  12878  sqr2irr  12886  absdvdsb  12906  dvdsle  12933  dvdseq  12935  dvdsext  12938  divalglem8  12958  divalglem9  12959  divalglem10  12960  divalgmod  12964  ndvdssub  12965  sadcaddlem  13007  gcdcllem1  13049  gcdcllem2  13050  gcdcllem3  13051  gcdeq  13090  dvdssq  13098  nn0seqcvgd  13099  algcvgblem  13106  1nprm  13122  1idssfct  13123  isprm2lem  13124  isprm2  13125  dvdsprime  13130  nprm  13131  3prm  13134  dvdsprm  13137  coprm  13138  exprmfct  13148  isprm5  13150  maxprmfct  13151  eulerthlem2  13209  odzval  13215  pythagtriplem4  13231  pc2dvds  13290  pcprmpw2  13293  pcprmpw  13294  prmpwdvds  13310  pockthg  13312  unbenlem  13314  prmreclem4  13325  prmreclem5  13326  prmreclem6  13327  1arith  13333  vdwlem6  13392  vdwlem11  13397  vdwlem13  13399  ramtlecl  13406  ramub  13419  rami  13421  ramubcl  13424  0ram  13426  ram0  13428  prmlem0  13466  prmlem1a  13467  imasaddfnlem  13791  imasvscafn  13800  imasleval  13804  prslem  14426  drsdir  14430  drsdirfi  14433  isdrs2  14434  posi  14445  posasymb  14447  pltval3  14462  plelttr  14467  pospo  14468  lubprop  14475  luble  14476  lubid  14477  glbprop  14480  joinval2  14484  joinlem  14485  meetlem  14492  meetle  14495  latnlej  14535  isglbd  14582  lubub  14584  lubun  14588  clatleglb  14591  pospropd  14599  poslubmo  14611  poslubd  14612  tsrlin  14689  spwmo  14696  spwpr2  14698  spwpr4  14701  letsr  14710  dirge  14720  mndodcongi  15219  odeq  15226  odmulgeq  15231  gexnnod  15260  sylow1lem1  15270  pgpssslw  15286  sylow2a  15291  efgredeu  15422  efgred2  15423  gexex  15506  frgpnabllem2  15523  cyggenod  15532  dprdval  15599  ablfacrplem  15661  ablfac1c  15667  ablfac1eu  15669  ablfaclem3  15683  abvtrivd  15966  psrbagconcl  16476  psrbagconf1o  16477  gsumbagdiaglem  16478  psrmulcllem  16489  psrlidm  16505  psrridm  16506  psrass1  16507  psrcom  16510  mplmonmul  16565  coe1mul2  16700  coe1tmmul  16707  zlpir  16809  prmirredlem  16811  znleval  16873  ordtbas2  17293  ordtopn2  17297  ordtrest2lem  17305  pnfnei  17322  ordtt1  17481  ordthauslem  17485  2ndci  17549  2ndcsb  17550  2ndcredom  17551  2ndc1stc  17552  1stcrest  17554  2ndcctbss  17556  2ndcdisj  17557  2ndcsep  17560  lly1stc  17597  tx1stc  17720  ordthmeolem  17871  ufildom1  17996  xmetrtri2  18424  prdsxmetlem  18436  ssblex  18496  prdsbl  18559  comet  18581  stdbdxmet  18583  stdbdmopn  18586  met1stc  18589  dscmet  18658  metdstri  18919  metdscn  18924  xrhmeo  19009  bndth  19021  evth  19022  lebnumlem3  19026  pcovalg  19075  pco1  19078  pcocn  19080  pcopt  19085  pcopt2  19086  pcoass  19087  nmoleub3  19165  bcthlem5  19319  minveclem4c  19364  minveclem2  19365  minveclem3b  19367  minveclem4  19371  minveclem6  19373  pmltpclem1  19383  pmltpc  19385  ovollb2lem  19422  ovolctb  19424  ovolunlem1  19431  ovoliunlem1  19436  ovoliunlem2  19437  ovoliun2  19440  ovolshftlem1  19443  ovolscalem1  19447  ovolicc1  19450  ovolicc2lem3  19453  voliunlem2  19483  voliunlem3  19484  ioombl1lem4  19493  uniioovol  19509  uniioombllem2  19513  uniioombllem3  19515  uniioombllem6  19518  volsup2  19535  ismbfd  19568  mbfsup  19592  mbflimsup  19594  itg1climres  19642  mbfi1fseqlem4  19646  itg2lr  19658  itg2leub  19662  itg2seq  19670  itg2monolem1  19678  itg2monolem3  19680  itg2mono  19681  itg2i1fseq2  19684  itg2gt0  19688  itg2cnlem1  19689  itg2cnlem2  19690  itg2cn  19691  iblss  19732  itgless  19744  ibladdlem  19747  iblabsr  19757  iblmulc2  19758  itgabs  19762  ditgeq1  19773  dvferm2lem  19908  rolle  19912  dvlip2  19917  c1liplem1  19918  c1lip1  19919  dvfsumlem2  19949  dvfsumlem4  19951  mdegleb  20025  degltlem1  20033  plyco0  20149  plyeq0lem  20167  coeeq2  20199  dgrle  20200  dgradd2  20224  plydiveu  20253  aareccl  20281  aalioulem2  20288  aaliou3lem7  20304  psercnlem1  20379  pilem2  20406  pilem3  20407  logltb  20532  divlogrlim  20564  logcnlem3  20573  cxpaddlelem  20673  rlimcnp  20842  cxplim  20848  cxploglim  20854  scvxcvx  20862  ftalem1  20893  ftalem2  20894  isppw2  20936  vmappw  20937  sgmnncl  20968  sqff1o  21003  dvdsdivcl  21004  fsumdvdsdiaglem  21006  dvdsppwf1o  21009  dvdsflsumcom  21011  musum  21014  muinv  21016  dvdsmulf1o  21017  vmalelog  21027  vmasum  21038  logfac2  21039  perfectlem2  21052  bcmono  21099  bpos1lem  21104  bposlem9  21114  lgsmod  21143  lgsne0  21155  2sqlem6  21191  2sqlem8  21194  2sqlem10  21196  chtppilim  21207  rpvmasumlem  21219  dchrisumlema  21220  dchrisumlem2  21222  dchrvmasumlem1  21227  dchrvmasumiflem1  21233  dchrisum0flblem1  21240  dchrisum0flblem2  21241  dchrisum0  21252  rplogsum  21259  logsqvma  21274  pntpbnd1  21318  pntpbnd2  21319  pntibndlem3  21324  pntlemj  21335  pntlemi  21336  pntlem3  21341  pnt3  21344  ostth3  21370  usgra1v  21447  usgrafisindb0  21460  usgrafisindb1  21461  cusgra1v  21508  1conngra  21700  eupath2  21740  gxnval  21886  rngosn4  22053  rngoueqz  22056  nmoubi  22311  minvecolem2  22415  minvecolem3  22416  minvecolem4c  22419  minvecolem4  22420  minvecolem5  22421  minvecolem6  22422  htthlem  22458  chlimi  22775  chcompl  22783  hsn0elch  22788  cmbr3  23148  cmcm  23154  cmcm3  23155  lecm  23157  nmopub  23449  nmfnleub  23466  nmopun  23555  nmcexi  23567  cnlnadjlem7  23614  pjnmopi  23689  stle0i  23780  stlesi  23782  stm1i  23784  csmdsymi  23875  cvmd  23877  atcveq0  23889  atcv1  23921  atord  23929  atcvat2  23930  chirred  23936  mdsym  23953  mddmdin0i  23972  cdj1i  23974  fmptcof2  24111  isoun  24124  lt2addrd  24150  xlt2addrd  24159  xrofsup  24161  tleile  24224  toslub  24226  tosglb  24227  ofldadd  24273  ofldmul  24274  xrnarchi  24289  xrge0iifiso  24356  rge0scvg  24370  gsumesum  24486  esumfsup  24495  esumpinfval  24498  esumpcvgval  24503  esumcvg  24511  sigaclcu  24535  sigaclci  24550  unelsiga  24552  measvun  24598  voliune  24620  volfiniune  24621  orvcval2  24751  dstfrvel  24766  ballotlemfc0  24785  ballotlemfcc  24786  ballotlemsv  24802  ballotlemsf1o  24806  relexpindlem  25174  rtrclreclem.trans  25181  dedekind  25222  dedekindle  25223  dfdm5  25435  dfrn5  25436  trpredpred  25541  poseq  25563  wsuclem  25611  nodense  25679  nocvxminlem  25680  nobnddown  25691  nofulllem4  25695  nofulllem5  25696  brpprod  25765  brsset  25769  brbigcup  25778  dffix2  25785  elfuns  25795  brimageg  25807  brdomaing  25815  brrangeg  25816  brimg  25817  brapply  25818  brsuccf  25821  funpartlem  25822  brrestrict  25829  dfrdg4  25830  axlowdim2  25934  axlowdim  25935  axcontlem2  25939  axcontlem3  25940  axcontlem4  25941  axcontlem7  25944  axcontlem9  25946  axcontlem10  25947  axcontlem11  25948  axcontlem12  25949  brofs  25974  btwncomim  25982  btwnintr  25988  btwnexch3  25989  btwnexch2  25992  brifs  26012  brcolinear2  26027  colineardim1  26030  brfs  26048  btwnconn1  26070  segcon2  26074  seglerflx  26081  seglemin  26082  btwnsegle  26086  colinbtwnle  26087  broutsideof2  26091  fvray  26110  lineunray  26116  lineelsb2  26117  linerflx1  26118  supaddc  26273  supadd  26274  ltflcei  26275  lxflflp1  26277  heicant  26281  mblfinlem1  26283  mblfinlem2  26284  itg2addnclem  26298  itg2addnclem3  26300  itg2addnc  26301  itg2gt0cn  26302  ibladdnclem  26303  iblmulc2nc  26312  itgabsnc  26316  bddiblnc  26317  ftc1anclem5  26326  ftc1anclem7  26328  ftc1anclem8  26329  ftc1anc  26330  trer  26361  elicc3  26362  finminlem  26363  nn0prpwlem  26367  nn0prpw  26368  indexdom  26478  filbcmb  26484  fdc  26491  prdsbnd  26544  heiborlem3  26564  rrnequiv  26586  prtlem10  26826  lzenom  26940  fphpdo  26990  irrapxlem4  27000  pellexlem6  27009  infmrgelbi  27053  pellfundre  27056  pellfundlb  27059  monotoddzz  27118  zindbi  27121  divalgmodcl  27170  jm2.27  27191  rmydioph  27197  rpnnen3lem  27214  fnwe2lem2  27238  aomclem8  27248  hbtlem5  27421  hbt  27423  pmtrval  27483  pmtrrn  27488  pmtrfrn  27489  phisum  27607  stoweidlem5  27842  stoweidlem20  27857  stoweidlem26  27863  stoweidlem28  27865  stoweidlem29  27866  stoweidlem34  27871  wallispilem3  27904  stirlinglem13  27923  funressnfv  28080  dfdfat2  28083  tz6.12-afv  28125  isfrgra  28552  3vfriswmgra  28567  1to2vfriswmgra  28568  vdfrgra0  28584  vdgfrgra0  28585  sgnval  28690  bnj23  29257  bnj1185  29339  bnj1152  29541  bnj1418  29583  lubunNEW  29945  lsatcveq0  30004  lsatcv1  30020  oposlem  30155  opnlen0  30160  lub0N  30161  glb0N  30165  omllaw  30215  cmtbr4N  30227  cvrval  30241  cvrnbtwn  30243  cvrnbtwn2  30247  cvrnbtwn3  30248  cvrcon3b  30249  cvrnbtwn4  30251  atcvreq0  30286  atnle  30289  atlatmstc  30291  cvlexch1  30300  glbconN  30348  hlsuprexch  30352  exatleN  30375  cvratlem  30392  atcvrj0  30399  atcvrj2b  30403  atlelt  30409  cvrat4  30414  3dim1lem5  30437  3dim2  30439  3dim3  30440  ps-2  30449  llni  30479  llnn0  30487  llnle  30489  lplni  30503  lplni2  30508  lplnle  30511  lplnn0N  30518  llncvrlpln  30529  2llnjN  30538  lvoli  30546  lvoli3  30548  lvoli2  30552  lvoln0N  30562  4at  30584  lplncvrlvol  30587  2lplnj  30591  dalemcea  30631  dalem3  30635  psubspi  30718  linepsubN  30723  elpmap  30729  pmapsub  30739  lnatexN  30750  cdlema1N  30762  cdlemb  30765  elpadd  30770  paddvaln0N  30772  paddasslem5  30795  llnexchb2lem  30839  llnexch2N  30841  islhp  30967  lhpat3  31017  4atexlemex2  31042  4atex  31047  4atex2-0aOLDN  31049  4atex2-0cOLDN  31051  lautle  31055  lautcvr  31063  lauteq  31066  ldilval  31084  ltrnu  31092  trlval2  31134  trlne  31156  cdleme0ex1N  31194  cdleme0nex  31261  cdleme18d  31266  cdlemednuN  31271  cdleme25b  31325  cdleme25cv  31329  cdleme27b  31339  cdleme29b  31346  cdleme31sn  31351  cdleme31fv  31361  cdleme31fv2  31364  cdlemefrs29bpre0  31367  cdlemefr29bpre0N  31377  cdlemefr29clN  31378  cdlemefr32fvaN  31380  cdlemefr32fva1  31381  cdlemefs29pre00N  31383  cdlemefs32sn1aw  31385  cdlemefs29bpre0N  31387  cdlemefs29bpre1N  31388  cdlemefs29cpre1N  31389  cdlemefs29clN  31390  cdlemefs32fvaN  31393  cdlemefs32fva1  31394  cdleme41sn3a  31404  cdleme32fva  31408  cdleme32e  31416  cdleme35f  31425  cdleme40v  31440  cdleme42b  31449  trlord  31540  cdlemg1cex  31559  diaval  32004  diaeldm  32008  diaelrnN  32017  cdlemm10N  32090  dibglbN  32138  dicval  32148  dicfnN  32155  dicvalrelN  32157  dihval  32204  dihlsscpre  32206  dihglblem3N  32267  dihmeetlem2N  32271  djhcvat42  32387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-br 4244
  Copyright terms: Public domain W3C validator