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  5909  foeqcnvco  5931  isorel  5949  isocnv  5952  isotr  5957  isoini  5959  isopolem  5963  isosolem  5965  f1oiso  5967  f1oiso2  5968  caovordig  6188  caovordg  6190  caovord3d  6193  caovord  6194  caovord3  6196  caofrss  6267  caoftrn  6268  poxp  6397  brtpos2  6417  rntpos  6423  tpostpos  6430  ertr  6717  ecopovsym  6800  ecopovtrn  6801  ecopovsymg  6803  ecopovtrng  6804  th3qlem2  6807  isfi  6934  en0  6969  en1  6973  en1bg  6974  endisj  7008  xpcomco  7010  dom0  7024  ssenen  7037  nneneq  7043  domfiexmid  7067  findcard  7077  findcard2  7078  findcard2s  7079  isinfinf  7086  tridc  7089  fimax2gtrilemstep  7090  fimax2gtri  7091  fiintim  7123  fisseneq  7127  en1eqsnbi  7148  isbth  7166  supmoti  7192  eqsupti  7195  supubti  7198  suplubti  7199  supsnti  7204  isotilem  7205  isoti  7206  supisolem  7207  supisoex  7208  infminti  7226  isnumi  7386  cardval3ex  7389  oncardval  7390  cardonle  7391  en2prde  7398  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidapne  7479  nqtri3or  7616  ltsonq  7618  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  subhalfnqq  7634  ltbtwnnqq  7635  archnqq  7637  nqnq0pi  7658  prcdnql  7704  prcunqu  7705  prnmaxl  7708  genpcuu  7740  genprndl  7741  genprndu  7742  nqprm  7762  nqprrnd  7763  nqprdisj  7764  nqprloc  7765  nqpru  7772  addnqprlemrl  7777  addnqprlemfl  7779  addnqprlemfu  7780  prmuloc2  7787  mulnqprlemrl  7793  mulnqprlemfl  7795  mulnqprlemfu  7796  1idprl  7810  ltnqpr  7813  ltnqpri  7814  prplnqu  7840  recexprlemell  7842  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssu  7854  recexprlemss1l  7855  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemladdfl  7875  cauappcvgprlem2  7880  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgprpr  7932  suplocexprlemmu  7938  suplocexprlemloc  7941  suplocexpr  7945  lttrsr  7982  ltsosr  7984  1ne0sr  7986  ltasrg  7990  aptisr  7999  mulextsr1  8001  archsr  8002  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axpre-ltwlin  8103  axpre-lttrn  8104  axpre-apti  8105  axpre-ltadd  8106  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  axcaucvg  8120  axpre-suploclemres  8121  axpre-suploc  8122  ltxrlt  8245  lttri3  8259  ltordlem  8662  lt0ne0d  8693  reapti  8759  apreim  8783  apsscn  8827  recexap  8833  lbreu  9125  lble  9127  suprleubex  9134  sup3exmid  9137  nnsub  9182  nominpos  9382  nn0n0n1ge2b  9559  zextle  9571  fzind  9595  btwnz  9599  uzval  9757  supinfneg  9829  infsupneg  9830  infregelbex  9832  ublbneg  9847  lbzbi  9850  qreccl  9876  xrltnsym  10028  xrlttr  10030  xrltso  10031  xrlttri3  10032  nltpnft  10049  npnflt  10050  xrrebnd  10054  xltnegi  10070  xnn0lenn0nn0  10100  xsubge0  10116  xlesubadd  10118  xleaddadd  10122  ixxval  10131  elixx1  10132  elioo2  10156  iccid  10160  fzval  10245  elfz1  10248  zsupcllemstep  10490  suprzubdc  10497  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  rebtwn2z  10515  qbtwnre  10517  qbtwnxr  10518  flval  10533  flqlelt  10537  flqbi  10551  flqeqceilz  10581  modqid2  10614  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2  10783  expcl2lemap  10814  expclzaplem  10826  expclzap  10827  expap0i  10834  nn0ltexp2  10972  hashinfuni  11040  hashennnuni  11042  hashunlem  11068  zfz1isolemiso  11104  zfz1isolem1  11105  zfz1iso  11106  absle  11667  maxleast  11791  rexanre  11798  rexico  11799  fimaxre2  11805  minmax  11808  xrmaxltsup  11836  xrminmax  11843  climshft  11882  reccn2ap  11891  summodclem3  11959  summodclem2a  11960  summodc  11962  zsumdc  11963  fsum3  11966  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  sumsnf  11988  fsummulc2  12027  isumlessdc  12075  cvgratz  12111  mertenslemi1  12114  ntrivcvgap0  12128  prodmodclem3  12154  prodmodclem2a  12155  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  fprodmul  12170  prodsnf  12171  absdvdsb  12388  zdvdsdc  12391  dvdsabseq  12426  dvdsdivcl  12429  dvdsext  12434  divalglemnn  12497  divalglemeunn  12500  divalglemeuneg  12502  divalgmod  12506  ndvdssub  12509  gcdsupex  12546  gcdsupcl  12547  gcddvds  12552  dvdslegcd  12553  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemzz  12591  bezoutlemmo  12595  bezoutlemeu  12596  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  dfgcd2  12603  gcdzeq  12611  dvdssq  12620  nnwodc  12625  uzwodc  12626  nnwofdc  12627  nn0seqcvgd  12631  algcvgblem  12639  lcmval  12653  lcmdvds  12669  lcmgcdeq  12673  coprmgcdb  12678  ncoprmgcdne1b  12679  coprmdvds1  12681  1nprm  12704  1idssfct  12705  isprm2lem  12706  isprm2  12707  dvdsprime  12712  nprm  12713  3prm  12718  dvdsprm  12727  exprmfct  12728  isprm5lem  12731  isprm5  12732  coprm  12734  sqrt2irr  12752  dvdsfi  12829  phisum  12831  odzval  12832  pythagtriplem4  12859  pc2dvds  12921  pcprmpw2  12924  pcprmpw  12925  dvdsprmpweqle  12928  oddprmdvds  12945  prmpwdvds  12946  pockthg  12948  1arith  12958  exmidunben  13065  nninfdclemcl  13087  nninfdclemp1  13089  nninfdc  13092  imasaddfnlemg  13415  cnfldui  14622  znleval  14686  ssblex  15174  comet  15242  bdmopn  15247  reopnap  15289  divcnap  15308  cdivcncfap  15347  cnopnap  15354  divcncfap  15357  maxcncf  15358  mincncf  15359  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeulemeu  15365  dedekindeu  15366  suplociccreex  15367  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemeu  15374  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  dich0  15395  ivthdich  15396  limcdifap  15405  limcimolemlt  15407  limccoap  15421  dvlemap  15423  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  dveflem  15469  logltb  15617  2irrexpqap  15721  sgmnncl  15731  dvdsppwf1o  15732  mpodvdsmulf1o  15733  perfectlem2  15743  lgsmod  15774  lgsne0  15786  gausslemma2dlem4  15812  2sqlem6  15868  2sqlem8  15871  2sqlem10  15873  upgrm  15970  upgr1or2  15971  umgredg2en  15979  umgrbien  15980  upgr1elem1  15990  umgr1een  15995  edgupgren  16011  edgumgren  16012  umgredgnlp  16022  edgusgren  16033  usgruspgrben  16056  usgr1e  16111  subumgredg2en  16141  subupgr  16143  wlkvtxiedg  16215  wlkvtxiedgg  16216  istrl  16255  iseupth  16317  eupth2fi  16349  konigsberglem1  16358  pw1nct  16655  sbthom  16681  trilpo  16698  trirec0  16699  reap0  16714  cndcap  16715  dcapnconst  16717  neapmkv  16724  neap0mkv  16725  ltlenmkv  16726