Theorem breq1 4091

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq1	⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Proof of Theorem breq1

Step	Hyp	Ref	Expression
1		opeq1 3862	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2300	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 4089	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4089	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ⟨cop 3672   class class class wbr 4088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breq12  4093  breq1i  4095  breq1d  4098  nbrne2  4108  brab1  4136  pocl  4400  swopolem  4402  swopo  4403  issod  4416  sowlin  4417  sotritrieq  4422  frirrg  4447  wetriext  4675  vtoclr  4774  brcog  4897  brcogw  4899  opelcnvg  4910  dfdmf  4924  eldmg  4926  dfrnf  4973  dfres2  5065  imasng  5101  coi1  5252  dffun6f  5339  funmo  5341  fun11  5397  fveq2  5639  funfveu  5652  sefvex  5660  nfunsn  5676  fvmptss2  5721  f1ompt  5798  fmptco  5813  dff13  5908  foeqcnvco  5930  isorel  5948  isocnv  5951  isotr  5956  isoini  5958  isopolem  5962  isosolem  5964  f1oiso  5966  f1oiso2  5967  caovordig  6187  caovordg  6189  caovord3d  6192  caovord  6193  caovord3  6195  caofrss  6266  caoftrn  6267  poxp  6396  brtpos2  6416  rntpos  6422  tpostpos  6429  ertr  6716  ecopovsym  6799  ecopovtrn  6800  ecopovsymg  6802  ecopovtrng  6803  th3qlem2  6806  isfi  6933  en0  6968  en1  6972  en1bg  6973  endisj  7007  xpcomco  7009  dom0  7023  ssenen  7036  nneneq  7042  domfiexmid  7066  findcard  7076  findcard2  7077  findcard2s  7078  isinfinf  7085  tridc  7088  fimax2gtrilemstep  7089  fimax2gtri  7090  fiintim  7122  fisseneq  7126  en1eqsnbi  7147  isbth  7165  supmoti  7191  eqsupti  7194  supubti  7197  suplubti  7198  supsnti  7203  isotilem  7204  isoti  7205  supisolem  7206  supisoex  7207  infminti  7225  isnumi  7385  cardval3ex  7388  oncardval  7389  cardonle  7390  en2prde  7397  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidapne  7478  nqtri3or  7615  ltsonq  7617  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  subhalfnqq  7633  ltbtwnnqq  7634  archnqq  7636  nqnq0pi  7657  prcdnql  7703  prcunqu  7704  prnmaxl  7707  genpcuu  7739  genprndl  7740  genprndu  7741  nqprm  7761  nqprrnd  7762  nqprdisj  7763  nqprloc  7764  nqpru  7771  addnqprlemrl  7776  addnqprlemfl  7778  addnqprlemfu  7779  prmuloc2  7786  mulnqprlemrl  7792  mulnqprlemfl  7794  mulnqprlemfu  7795  1idprl  7809  ltnqpr  7812  ltnqpri  7813  prplnqu  7839  recexprlemell  7841  recexprlemm  7843  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssu  7853  recexprlemss1l  7854  aptiprlemu  7859  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemladdfl  7874  cauappcvgprlem2  7879  cauappcvgpr  7881  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemcl  7895  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnbj  7912  caucvgprprlemmu  7914  caucvgprprlemopu  7918  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgprpr  7931  suplocexprlemmu  7937  suplocexprlemloc  7940  suplocexpr  7944  lttrsr  7981  ltsosr  7983  1ne0sr  7985  ltasrg  7989  aptisr  7998  mulextsr1  8000  archsr  8001  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axpre-ltwlin  8102  axpre-lttrn  8103  axpre-apti  8104  axpre-ltadd  8105  axpre-mulext  8107  axcaucvglemcau  8117  axcaucvglemres  8118  axcaucvg  8119  axpre-suploclemres  8120  axpre-suploc  8121  ltxrlt  8244  lttri3  8258  ltordlem  8661  lt0ne0d  8692  reapti  8758  apreim  8782  apsscn  8826  recexap  8832  lbreu  9124  lble  9126  suprleubex  9133  sup3exmid  9136  nnsub  9181  nominpos  9381  nn0n0n1ge2b  9558  zextle  9570  fzind  9594  btwnz  9598  uzval  9756  supinfneg  9828  infsupneg  9829  infregelbex  9831  ublbneg  9846  lbzbi  9849  qreccl  9875  xrltnsym  10027  xrlttr  10029  xrltso  10030  xrlttri3  10031  nltpnft  10048  npnflt  10049  xrrebnd  10053  xltnegi  10069  xnn0lenn0nn0  10099  xsubge0  10115  xlesubadd  10117  xleaddadd  10121  ixxval  10130  elixx1  10131  elioo2  10155  iccid  10159  fzval  10244  elfz1  10247  zsupcllemstep  10488  suprzubdc  10495  zsupssdc  10497  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemshrink  10507  exbtwnzlemex  10508  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2zlemshrink  10512  rebtwn2z  10513  qbtwnre  10515  qbtwnxr  10516  flval  10531  flqlelt  10535  flqbi  10549  flqeqceilz  10579  modqid2  10612  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem2  10781  expcl2lemap  10812  expclzaplem  10824  expclzap  10825  expap0i  10832  nn0ltexp2  10970  hashinfuni  11038  hashennnuni  11040  hashunlem  11066  zfz1isolemiso  11102  zfz1isolem1  11103  zfz1iso  11104  absle  11649  maxleast  11773  rexanre  11780  rexico  11781  fimaxre2  11787  minmax  11790  xrmaxltsup  11818  xrminmax  11825  climshft  11864  reccn2ap  11873  summodclem3  11940  summodclem2a  11941  summodc  11943  zsumdc  11944  fsum3  11947  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  sumsnf  11969  fsummulc2  12008  isumlessdc  12056  cvgratz  12092  mertenslemi1  12095  ntrivcvgap0  12109  prodmodclem3  12135  prodmodclem2a  12136  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  fprodmul  12151  prodsnf  12152  absdvdsb  12369  zdvdsdc  12372  dvdsabseq  12407  dvdsdivcl  12410  dvdsext  12415  divalglemnn  12478  divalglemeunn  12481  divalglemeuneg  12483  divalgmod  12487  ndvdssub  12490  gcdsupex  12527  gcdsupcl  12528  gcddvds  12533  dvdslegcd  12534  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemmo  12576  bezoutlemeu  12577  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  dfgcd2  12584  gcdzeq  12592  dvdssq  12601  nnwodc  12606  uzwodc  12607  nnwofdc  12608  nn0seqcvgd  12612  algcvgblem  12620  lcmval  12634  lcmdvds  12650  lcmgcdeq  12654  coprmgcdb  12659  ncoprmgcdne1b  12660  coprmdvds1  12662  1nprm  12685  1idssfct  12686  isprm2lem  12687  isprm2  12688  dvdsprime  12693  nprm  12694  3prm  12699  dvdsprm  12708  exprmfct  12709  isprm5lem  12712  isprm5  12713  coprm  12715  sqrt2irr  12733  dvdsfi  12810  phisum  12812  odzval  12813  pythagtriplem4  12840  pc2dvds  12902  pcprmpw2  12905  pcprmpw  12906  dvdsprmpweqle  12909  oddprmdvds  12926  prmpwdvds  12927  pockthg  12929  1arith  12939  exmidunben  13046  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  imasaddfnlemg  13396  cnfldui  14602  znleval  14666  ssblex  15154  comet  15222  bdmopn  15227  reopnap  15269  divcnap  15288  cdivcncfap  15327  cnopnap  15334  divcncfap  15337  maxcncf  15338  mincncf  15339  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeulemeu  15345  dedekindeu  15346  suplociccreex  15347  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemeu  15354  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  dich0  15375  ivthdich  15376  limcdifap  15385  limcimolemlt  15387  limccoap  15401  dvlemap  15403  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  dveflem  15449  logltb  15597  2irrexpqap  15701  sgmnncl  15711  dvdsppwf1o  15712  mpodvdsmulf1o  15713  perfectlem2  15723  lgsmod  15754  lgsne0  15766  gausslemma2dlem4  15792  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  upgrm  15950  upgr1or2  15951  umgredg2en  15959  umgrbien  15960  upgr1elem1  15970  umgr1een  15975  edgupgren  15991  edgumgren  15992  umgredgnlp  16002  edgusgren  16013  usgruspgrben  16036  usgr1e  16091  subumgredg2en  16121  subupgr  16123  wlkvtxiedg  16195  wlkvtxiedgg  16196  istrl  16235  iseupth  16297  pw1nct  16604  sbthom  16630  trilpo  16647  trirec0  16648  reap0  16662  cndcap  16663  dcapnconst  16665  neapmkv  16672  neap0mkv  16673  ltlenmkv  16674