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  7262  cardval3ex  7265  oncardval  7266  cardonle  7267  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidapne  7345  nqtri3or  7482  ltsonq  7484  ltanqg  7486  ltmnqg  7487  ltexnqq  7494  subhalfnqq  7500  ltbtwnnqq  7501  archnqq  7503  nqnq0pi  7524  prcdnql  7570  prcunqu  7571  prnmaxl  7574  genpcuu  7606  genprndl  7607  genprndu  7608  nqprm  7628  nqprrnd  7629  nqprdisj  7630  nqprloc  7631  nqpru  7638  addnqprlemrl  7643  addnqprlemfl  7645  addnqprlemfu  7646  prmuloc2  7653  mulnqprlemrl  7659  mulnqprlemfl  7661  mulnqprlemfu  7662  1idprl  7676  ltnqpr  7679  ltnqpri  7680  prplnqu  7706  recexprlemell  7708  recexprlemm  7710  recexprlemdisj  7716  recexprlemloc  7717  recexprlem1ssu  7720  recexprlemss1l  7721  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemladdfl  7741  cauappcvgprlem2  7746  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemcl  7762  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemelu  7772  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnbj  7779  caucvgprprlemmu  7781  caucvgprprlemopu  7785  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlem1  7795  caucvgprprlem2  7796  caucvgprpr  7798  suplocexprlemmu  7804  suplocexprlemloc  7807  suplocexpr  7811  lttrsr  7848  ltsosr  7850  1ne0sr  7852  ltasrg  7856  aptisr  7865  mulextsr1  7867  archsr  7868  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  caucvgsr  7888  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axpre-ltwlin  7969  axpre-lttrn  7970  axpre-apti  7971  axpre-ltadd  7972  axpre-mulext  7974  axcaucvglemcau  7984  axcaucvglemres  7985  axcaucvg  7986  axpre-suploclemres  7987  axpre-suploc  7988  ltxrlt  8111  lttri3  8125  ltordlem  8528  lt0ne0d  8559  reapti  8625  apreim  8649  apsscn  8693  recexap  8699  lbreu  8991  lble  8993  suprleubex  9000  sup3exmid  9003  nnsub  9048  nominpos  9248  nn0n0n1ge2b  9424  zextle  9436  fzind  9460  btwnz  9464  uzval  9622  supinfneg  9688  infsupneg  9689  infregelbex  9691  ublbneg  9706  lbzbi  9709  qreccl  9735  xrltnsym  9887  xrlttr  9889  xrltso  9890  xrlttri3  9891  nltpnft  9908  npnflt  9909  xrrebnd  9913  xltnegi  9929  xnn0lenn0nn0  9959  xsubge0  9975  xlesubadd  9977  xleaddadd  9981  ixxval  9990  elixx1  9991  elioo2  10015  iccid  10019  fzval  10104  elfz1  10107  zsupcllemstep  10338  suprzubdc  10345  zsupssdc  10347  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemshrink  10357  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2zlemshrink  10362  rebtwn2z  10363  qbtwnre  10365  qbtwnxr  10366  flval  10381  flqlelt  10385  flqbi  10399  flqeqceilz  10429  modqid2  10462  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem2  10631  expcl2lemap  10662  expclzaplem  10674  expclzap  10675  expap0i  10682  nn0ltexp2  10820  hashinfuni  10888  hashennnuni  10890  hashunlem  10915  zfz1isolemiso  10950  zfz1isolem1  10951  zfz1iso  10952  absle  11273  maxleast  11397  rexanre  11404  rexico  11405  fimaxre2  11411  minmax  11414  xrmaxltsup  11442  xrminmax  11449  climshft  11488  reccn2ap  11497  summodclem3  11564  summodclem2a  11565  summodc  11567  zsumdc  11568  fsum3  11571  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  sumsnf  11593  fsummulc2  11632  isumlessdc  11680  cvgratz  11716  mertenslemi1  11719  ntrivcvgap0  11733  prodmodclem3  11759  prodmodclem2a  11760  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  fprodmul  11775  prodsnf  11776  absdvdsb  11993  zdvdsdc  11996  dvdsabseq  12031  dvdsdivcl  12034  dvdsext  12039  divalglemnn  12102  divalglemeunn  12105  divalglemeuneg  12107  divalgmod  12111  ndvdssub  12114  gcdsupex  12151  gcdsupcl  12152  gcddvds  12157  dvdslegcd  12158  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemmo  12200  bezoutlemeu  12201  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  dfgcd2  12208  gcdzeq  12216  dvdssq  12225  nnwodc  12230  uzwodc  12231  nnwofdc  12232  nn0seqcvgd  12236  algcvgblem  12244  lcmval  12258  lcmdvds  12274  lcmgcdeq  12278  coprmgcdb  12283  ncoprmgcdne1b  12284  coprmdvds1  12286  1nprm  12309  1idssfct  12310  isprm2lem  12311  isprm2  12312  dvdsprime  12317  nprm  12318  3prm  12323  dvdsprm  12332  exprmfct  12333  isprm5lem  12336  isprm5  12337  coprm  12339  sqrt2irr  12357  dvdsfi  12434  phisum  12436  odzval  12437  pythagtriplem4  12464  pc2dvds  12526  pcprmpw2  12529  pcprmpw  12530  dvdsprmpweqle  12533  oddprmdvds  12550  prmpwdvds  12551  pockthg  12553  1arith  12563  exmidunben  12670  nninfdclemcl  12692  nninfdclemp1  12694  nninfdc  12697  imasaddfnlemg  13018  cnfldui  14223  znleval  14287  ssblex  14775  comet  14843  bdmopn  14848  reopnap  14890  divcnap  14909  cdivcncfap  14948  cnopnap  14955  divcncfap  14958  maxcncf  14959  mincncf  14960  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeulemeu  14966  dedekindeu  14967  suplociccreex  14968  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemeu  14975  dedekindicclemicc  14976  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthinc  14987  ivthreinc  14989  dich0  14996  ivthdich  14997  limcdifap  15006  limcimolemlt  15008  limccoap  15022  dvlemap  15024  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  dveflem  15070  logltb  15218  2irrexpqap  15322  sgmnncl  15332  dvdsppwf1o  15333  mpodvdsmulf1o  15334  perfectlem2  15344  lgsmod  15375  lgsne0  15387  gausslemma2dlem4  15413  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  pw1nct  15758  sbthom  15783  trilpo  15800  trirec0  15801  reap0  15815  cndcap  15816  dcapnconst  15818  neapmkv  15825  neap0mkv  15826  ltlenmkv  15827