Theorem breq1 4037

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 3809	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	eleq1d 2265	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐴, 𝐶⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
3		df-br 4035	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4035	. 2 ⊢ (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167  ⟨cop 3626   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breq12  4039  breq1i  4041  breq1d  4044  nbrne2  4054  brab1  4081  pocl  4339  swopolem  4341  swopo  4342  issod  4355  sowlin  4356  sotritrieq  4361  frirrg  4386  wetriext  4614  vtoclr  4712  brcog  4834  brcogw  4836  opelcnvg  4847  dfdmf  4860  eldmg  4862  dfrnf  4908  dfres2  4999  imasng  5035  coi1  5186  dffun6f  5272  funmo  5274  fun11  5326  fveq2  5561  funfveu  5574  sefvex  5582  nfunsn  5596  fvmptss2  5639  f1ompt  5716  fmptco  5731  dff13  5818  foeqcnvco  5840  isorel  5858  isocnv  5861  isotr  5866  isoini  5868  isopolem  5872  isosolem  5874  f1oiso  5876  f1oiso2  5877  caovordig  6093  caovordg  6095  caovord3d  6098  caovord  6099  caovord3  6101  caofrss  6171  caoftrn  6172  poxp  6299  brtpos2  6318  rntpos  6324  tpostpos  6331  ertr  6616  ecopovsym  6699  ecopovtrn  6700  ecopovsymg  6702  ecopovtrng  6703  th3qlem2  6706  isfi  6829  en0  6863  en1  6867  en1bg  6868  endisj  6892  xpcomco  6894  dom0  6908  ssenen  6921  nneneq  6927  domfiexmid  6948  findcard  6958  findcard2  6959  findcard2s  6960  isinfinf  6967  tridc  6969  fimax2gtrilemstep  6970  fimax2gtri  6971  fiintim  7001  fisseneq  7004  en1eqsnbi  7024  isbth  7042  supmoti  7068  eqsupti  7071  supubti  7074  suplubti  7075  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  infminti  7102  isnumi  7260  cardval3ex  7263  oncardval  7264  cardonle  7265  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidapne  7343  nqtri3or  7480  ltsonq  7482  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  subhalfnqq  7498  ltbtwnnqq  7499  archnqq  7501  nqnq0pi  7522  prcdnql  7568  prcunqu  7569  prnmaxl  7572  genpcuu  7604  genprndl  7605  genprndu  7606  nqprm  7626  nqprrnd  7627  nqprdisj  7628  nqprloc  7629  nqpru  7636  addnqprlemrl  7641  addnqprlemfl  7643  addnqprlemfu  7644  prmuloc2  7651  mulnqprlemrl  7657  mulnqprlemfl  7659  mulnqprlemfu  7660  1idprl  7674  ltnqpr  7677  ltnqpri  7678  prplnqu  7704  recexprlemell  7706  recexprlemm  7708  recexprlemdisj  7714  recexprlemloc  7715  recexprlem1ssu  7718  recexprlemss1l  7719  aptiprlemu  7724  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemladdfl  7739  cauappcvgprlem2  7744  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemcl  7760  caucvgprlem2  7764  caucvgpr  7766  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnbj  7777  caucvgprprlemmu  7779  caucvgprprlemopu  7783  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgprpr  7796  suplocexprlemmu  7802  suplocexprlemloc  7805  suplocexpr  7809  lttrsr  7846  ltsosr  7848  1ne0sr  7850  ltasrg  7854  aptisr  7863  mulextsr1  7865  archsr  7866  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axpre-ltwlin  7967  axpre-lttrn  7968  axpre-apti  7969  axpre-ltadd  7970  axpre-mulext  7972  axcaucvglemcau  7982  axcaucvglemres  7983  axcaucvg  7984  axpre-suploclemres  7985  axpre-suploc  7986  ltxrlt  8109  lttri3  8123  ltordlem  8526  lt0ne0d  8557  reapti  8623  apreim  8647  apsscn  8691  recexap  8697  lbreu  8989  lble  8991  suprleubex  8998  sup3exmid  9001  nnsub  9046  nominpos  9246  nn0n0n1ge2b  9422  zextle  9434  fzind  9458  btwnz  9462  uzval  9620  supinfneg  9686  infsupneg  9687  infregelbex  9689  ublbneg  9704  lbzbi  9707  qreccl  9733  xrltnsym  9885  xrlttr  9887  xrltso  9888  xrlttri3  9889  nltpnft  9906  npnflt  9907  xrrebnd  9911  xltnegi  9927  xnn0lenn0nn0  9957  xsubge0  9973  xlesubadd  9975  xleaddadd  9979  ixxval  9988  elixx1  9989  elioo2  10013  iccid  10017  fzval  10102  elfz1  10105  zsupcllemstep  10336  suprzubdc  10343  zsupssdc  10345  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemshrink  10355  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2zlemshrink  10360  rebtwn2z  10361  qbtwnre  10363  qbtwnxr  10364  flval  10379  flqlelt  10383  flqbi  10397  flqeqceilz  10427  modqid2  10460  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem2  10629  expcl2lemap  10660  expclzaplem  10672  expclzap  10673  expap0i  10680  nn0ltexp2  10818  hashinfuni  10886  hashennnuni  10888  hashunlem  10913  zfz1isolemiso  10948  zfz1isolem1  10949  zfz1iso  10950  absle  11271  maxleast  11395  rexanre  11402  rexico  11403  fimaxre2  11409  minmax  11412  xrmaxltsup  11440  xrminmax  11447  climshft  11486  reccn2ap  11495  summodclem3  11562  summodclem2a  11563  summodc  11565  zsumdc  11566  fsum3  11569  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  sumsnf  11591  fsummulc2  11630  isumlessdc  11678  cvgratz  11714  mertenslemi1  11717  ntrivcvgap0  11731  prodmodclem3  11757  prodmodclem2a  11758  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  fprodmul  11773  prodsnf  11774  absdvdsb  11991  zdvdsdc  11994  dvdsabseq  12029  dvdsdivcl  12032  dvdsext  12037  divalglemnn  12100  divalglemeunn  12103  divalglemeuneg  12105  divalgmod  12109  ndvdssub  12112  gcdsupex  12149  gcdsupcl  12150  gcddvds  12155  dvdslegcd  12156  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemmo  12198  bezoutlemeu  12199  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dfgcd2  12206  gcdzeq  12214  dvdssq  12223  nnwodc  12228  uzwodc  12229  nnwofdc  12230  nn0seqcvgd  12234  algcvgblem  12242  lcmval  12256  lcmdvds  12272  lcmgcdeq  12276  coprmgcdb  12281  ncoprmgcdne1b  12282  coprmdvds1  12284  1nprm  12307  1idssfct  12308  isprm2lem  12309  isprm2  12310  dvdsprime  12315  nprm  12316  3prm  12321  dvdsprm  12330  exprmfct  12331  isprm5lem  12334  isprm5  12335  coprm  12337  sqrt2irr  12355  dvdsfi  12432  phisum  12434  odzval  12435  pythagtriplem4  12462  pc2dvds  12524  pcprmpw2  12527  pcprmpw  12528  dvdsprmpweqle  12531  oddprmdvds  12548  prmpwdvds  12549  pockthg  12551  1arith  12561  exmidunben  12668  nninfdclemcl  12690  nninfdclemp1  12692  nninfdc  12695  imasaddfnlemg  13016  cnfldui  14221  znleval  14285  ssblex  14751  comet  14819  bdmopn  14824  reopnap  14866  divcnap  14885  cdivcncfap  14924  cnopnap  14931  divcncfap  14934  maxcncf  14935  mincncf  14936  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeulemeu  14942  dedekindeu  14943  suplociccreex  14944  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemeu  14951  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  dich0  14972  ivthdich  14973  limcdifap  14982  limcimolemlt  14984  limccoap  14998  dvlemap  15000  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  dveflem  15046  logltb  15194  2irrexpqap  15298  sgmnncl  15308  dvdsppwf1o  15309  mpodvdsmulf1o  15310  perfectlem2  15320  lgsmod  15351  lgsne0  15363  gausslemma2dlem4  15389  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  pw1nct  15734  sbthom  15757  trilpo  15774  trirec0  15775  reap0  15789  cndcap  15790  dcapnconst  15792  neapmkv  15799  neap0mkv  15800  ltlenmkv  15801