Theorem breq1 4133

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ⟨cop 3712   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq12  4135  breq1i  4137  breq1d  4140  nbrne2  4150  brab1  4178  pocl  4448  swopolem  4450  swopo  4451  issod  4464  sowlin  4465  sotritrieq  4470  frirrg  4495  wetriext  4724  vtoclr  4823  brcog  4947  brcogw  4949  opelcnvg  4960  dfdmf  4974  eldmg  4976  dfrnf  5023  dfres2  5115  imasng  5152  coi1  5303  dffun6f  5390  funmo  5392  fun11  5448  fveq2  5695  funfveu  5708  sefvex  5716  nfunsn  5733  fvmptss2  5780  f1ompt  5859  fmptco  5874  dff13  5974  foeqcnvco  5996  isorel  6014  isocnv  6017  isotr  6022  isoini  6024  isopolem  6028  isosolem  6030  f1oiso  6032  f1oiso2  6033  caovordig  6255  caovordg  6257  caovord3d  6260  caovord  6261  caovord3  6263  caofrss  6334  caoftrn  6335  poxp  6468  brtpos2  6522  rntpos  6528  tpostpos  6535  ertr  6822  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  th3qlem2  6912  isfi  7047  en0  7082  en1  7086  en1bg  7087  endisj  7122  xpcomco  7124  dom0  7138  ssenen  7152  nneneq  7158  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  tridc  7204  fimax2gtrilemstep  7205  fimax2gtri  7206  fiintim  7238  fisseneq  7242  en1eqsnbi  7266  isbth  7284  supmoti  7333  eqsupti  7336  supubti  7339  suplubti  7340  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  infminti  7367  isnumi  7527  cardval3ex  7530  oncardval  7531  cardonle  7532  en2prde  7539  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papsym  7612  papcotr  7613  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  subhalfnqq  7781  ltbtwnnqq  7782  archnqq  7784  nqnq0pi  7805  prcdnql  7851  prcunqu  7852  prnmaxl  7855  genpcuu  7887  genprndl  7888  genprndu  7889  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqpru  7919  addnqprlemrl  7924  addnqprlemfl  7926  addnqprlemfu  7927  prmuloc2  7934  mulnqprlemrl  7940  mulnqprlemfl  7942  mulnqprlemfu  7943  1idprl  7957  ltnqpr  7960  ltnqpri  7961  prplnqu  7987  recexprlemell  7989  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssu  8001  recexprlemss1l  8002  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexpr  8092  lttrsr  8129  ltsosr  8131  1ne0sr  8133  ltasrg  8137  aptisr  8146  mulextsr1  8148  archsr  8149  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-ltadd  8253  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axcaucvg  8267  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  lttri3  8405  ltordlem  8811  lt0ne0d  8842  reapti  8909  apreim  8933  apsscn  8977  recexap  8983  lbreu  9277  lble  9279  suprleubex  9286  sup3exmid  9289  nnsub  9345  nominpos  9547  nn0n0n1ge2b  9729  zextle  9741  fzind  9765  btwnz  9769  uzval  9932  supinfneg  10004  infsupneg  10005  infregelbex  10007  ublbneg  10022  lbzbi  10025  qreccl  10051  xrltnsym  10205  xrlttr  10207  xrltso  10208  xrlttri3  10209  nltpnft  10226  npnflt  10227  xrrebnd  10231  xltnegi  10247  xnn0lenn0nn0  10277  xsubge0  10293  xlesubadd  10295  xleaddadd  10299  ixxval  10308  elixx1  10309  elioo2  10333  iccid  10337  fzval  10423  elfz1  10426  zsupcllemstep  10672  suprzubdc  10681  zsupssdc  10683  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemshrink  10693  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2zlemshrink  10698  rebtwn2z  10699  qbtwnre  10701  qbtwnxr  10702  flval  10717  flqlelt  10722  flaplelt  10723  flqbi  10738  flqeqceilz  10768  modqid2  10801  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem2  10970  expcl2lemap  11001  expclzaplem  11013  expclzap  11014  expap0i  11021  nn0ltexp2  11161  hashinfuni  11230  hashennnuni  11232  hashunlem  11258  zfz1isolemiso  11305  zfz1isolem1  11306  zfz1iso  11307  absle  11870  maxleast  11994  rexanre  12001  rexico  12002  fimaxre2  12008  minmax  12011  xrmaxltsup  12040  xrminmax  12047  climshft  12086  reccn2ap  12095  summodclem3  12163  summodclem2a  12164  summodc  12166  zsumdc  12167  fsum3  12170  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  sumsnf  12192  fsummulc2  12231  isumlessdc  12279  cvgratz  12315  mertenslemi1  12318  ntrivcvgap0  12332  prodmodclem3  12358  prodmodclem2a  12359  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  fprodmul  12374  prodsnf  12375  absdvdsb  12592  zdvdsdc  12595  dvdsabseq  12630  dvdsdivcl  12633  dvdsext  12638  divalglemnn  12701  divalglemeunn  12704  divalglemeuneg  12706  divalgmod  12710  ndvdssub  12713  gcdsupex  12750  gcdsupcl  12751  gcddvds  12756  dvdslegcd  12757  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemmo  12799  bezoutlemeu  12800  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dfgcd2  12807  gcdzeq  12815  dvdssq  12824  nnwodc  12829  uzwodc  12830  nnwofdc  12831  nn0seqcvgd  12835  algcvgblem  12843  lcmval  12857  lcmdvds  12873  lcmgcdeq  12877  coprmgcdb  12882  ncoprmgcdne1b  12883  coprmdvds1  12885  1nprm  12908  1idssfct  12909  isprm2lem  12910  isprm2  12911  dvdsprime  12916  nprm  12917  3prm  12922  dvdsprm  12932  exprmfct  12933  isprm5lem  12936  isprm5  12937  coprm  12939  sqrt2irr  12957  dvdsfi  13037  phisum  13039  odzval  13040  pythagtriplem4  13067  pc2dvds  13129  pcprmpw2  13132  pcprmpw  13133  dvdsprmpweqle  13136  oddprmdvds  13153  prmpwdvds  13154  pockthg  13156  1arith  13166  prmlem0  13240  prmlem1a  13241  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsv  13302  ballotfilemsf1o  13306  ballotfi  13331  exmidunben  13366  nninfdclemcl  13388  nninfdclemp1  13390  nninfdc  13393  imasaddfnlemg  13684  ringunitsap0  14643  drnguiap  14658  cnfldui  14973  znleval  15037  psrbagconcl  15112  ssblex  15581  comet  15649  bdmopn  15654  reopnap  15696  divcnap  15715  cdivcncfap  15754  cnopnap  15761  divcncfap  15764  maxcncf  15765  mincncf  15766  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeulemeu  15772  dedekindeu  15773  suplociccreex  15774  dedekindicclemuub  15776  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemeu  15781  dedekindicclemicc  15782  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  dich0  15802  ivthdich  15803  limcdifap  15812  limcimolemlt  15814  limccoap  15828  dvlemap  15830  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  dveflem  15876  logltb  16026  2irrexpqap  16133  prmdvdsfi  16159  sgmnncl  16169  dvdsppwf1o  16184  mpodvdsmulf1o  16185  perfectlem2  16198  bcmono  16202  bpos1lem  16207  lgsmod  16243  lgsne0  16255  gausslemma2dlem4  16281  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  upgrm  16439  upgr1or2  16440  umgredg2en  16448  umgrbien  16449  upgr1elem1  16459  umgr1een  16464  edgupgren  16480  edgumgren  16481  umgredgnlp  16491  edgusgren  16502  usgruspgrben  16525  usgr1e  16580  subumgredg2en  16610  subupgr  16612  wlkvtxiedg  16684  wlkvtxiedgg  16685  istrl  16724  iseupth  16786  eupth2fi  16818  konigsberglem1  16827  lealltlt1  16849  pw1nct  17131  sbthom  17169  trilpo  17190  trirec0  17191  reap0  17206  cndcap  17207  dcapnconst  17209  neapmkv  17216  neap0mkv  17217  ltlenmkv  17218