Theorem breq1 4134

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 4132	. 2 ⊢ (𝐴𝑅𝐶 ↔ ⟨𝐴, 𝐶⟩ ∈ 𝑅)
4		df-br 4132	. 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 4131

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 4132

This theorem is used by:  breq12  4136  breq1i  4138  breq1d  4141  nbrne2  4151  brab1  4179  pocl  4450  swopolem  4452  swopo  4453  issod  4466  sowlin  4467  sotritrieq  4472  frirrg  4497  wetriext  4726  vtoclr  4825  brcog  4949  brcogw  4951  opelcnvg  4962  dfdmf  4976  eldmg  4978  dfrnf  5025  dfres2  5118  imasng  5155  coi1  5306  dffun6f  5393  funmo  5395  fun11  5451  fveq2  5698  funfveu  5711  sefvex  5719  nfunsn  5736  fvmptss2  5783  f1ompt  5862  fmptco  5877  dff13  5977  foeqcnvco  5999  isorel  6017  isocnv  6020  isotr  6025  isoini  6027  isopolem  6031  isosolem  6033  f1oiso  6035  f1oiso2  6036  caovordig  6258  caovordg  6260  caovord3d  6263  caovord  6264  caovord3  6266  caofrss  6338  caoftrn  6339  poxp  6472  brtpos2  6526  rntpos  6532  tpostpos  6539  ertr  6826  ecopovsym  6909  ecopovtrn  6910  ecopovsymg  6912  ecopovtrng  6913  th3qlem2  6916  isfi  7051  en0  7086  en1  7090  en1bg  7091  endisj  7126  xpcomco  7128  dom0  7142  ssenen  7156  nneneq  7162  domfiexmid  7186  findcard  7196  findcard2  7197  findcard2s  7198  isinfinf  7205  tridc  7208  fimax2gtrilemstep  7209  fimax2gtri  7210  fiintim  7242  fisseneq  7246  en1eqsnbi  7271  isbth  7289  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  infminti  7373  isnumi  7533  cardval3ex  7536  oncardval  7537  cardonle  7538  en2prde  7545  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  papsym  7618  papcotr  7619  exmidapne  7632  nqtri3or  7769  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  subhalfnqq  7787  ltbtwnnqq  7788  archnqq  7790  nqnq0pi  7811  prcdnql  7857  prcunqu  7858  prnmaxl  7861  genpcuu  7893  genprndl  7894  genprndu  7895  nqprm  7915  nqprrnd  7916  nqprdisj  7917  nqprloc  7918  nqpru  7925  addnqprlemrl  7930  addnqprlemfl  7932  addnqprlemfu  7933  prmuloc2  7940  mulnqprlemrl  7946  mulnqprlemfl  7948  mulnqprlemfu  7949  1idprl  7963  ltnqpr  7966  ltnqpri  7967  prplnqu  7993  recexprlemell  7995  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssu  8007  recexprlemss1l  8008  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemladdfl  8028  cauappcvgprlem2  8033  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgprlem2  8053  caucvgpr  8055  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgprpr  8085  suplocexprlemmu  8091  suplocexprlemloc  8094  suplocexpr  8098  lttrsr  8135  ltsosr  8137  1ne0sr  8139  ltasrg  8143  aptisr  8152  mulextsr1  8154  archsr  8155  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-ltwlin  8256  axpre-lttrn  8257  axpre-apti  8258  axpre-ltadd  8259  axpre-mulext  8261  axcaucvglemcau  8271  axcaucvglemres  8272  axcaucvg  8273  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  lttri3  8411  ltordlem  8817  lt0ne0d  8848  reapti  8915  apreim  8939  apsscn  8983  recexap  8989  lbreu  9283  lble  9285  suprleubex  9292  sup3exmid  9295  nnsub  9352  nominpos  9554  nn0n0n1ge2b  9736  zextle  9748  fzind  9772  btwnz  9776  uzval  9939  supinfneg  10011  infsupneg  10012  infregelbex  10014  ublbneg  10029  lbzbi  10032  qreccl  10058  xrltnsym  10212  xrlttr  10214  xrltso  10215  xrlttri3  10216  nltpnft  10233  npnflt  10234  xrrebnd  10238  xltnegi  10254  xnn0lenn0nn0  10284  xsubge0  10300  xlesubadd  10302  xleaddadd  10306  ixxval  10315  elixx1  10316  elioo2  10340  iccid  10344  fzval  10430  elfz1  10433  zsupcllemstep  10679  suprzubdc  10688  zsupssdc  10690  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemshrink  10700  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2zlemshrink  10705  rebtwn2z  10706  qbtwnre  10708  qbtwnxr  10709  flval  10724  flqlelt  10729  flaplelt  10730  flqbi  10746  flqeqceilz  10776  modqid2  10809  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem2  10978  expcl2lemap  11009  expclzaplem  11021  expclzap  11022  expap0i  11029  nn0ltexp2  11169  hashinfuni  11238  hashennnuni  11240  hashunlem  11266  zfz1isolemiso  11313  zfz1isolem1  11314  zfz1iso  11315  absle  11878  maxleast  12002  rexanre  12009  rexico  12010  fimaxre2  12016  minmax  12020  xrmaxltsup  12049  xrminmax  12056  climshft  12095  reccn2ap  12104  summodclem3  12172  summodclem2a  12173  summodc  12175  zsumdc  12176  fsum3  12179  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  sumsnf  12201  fsummulc2  12240  isumlessdc  12288  cvgratz  12324  mertenslemi1  12327  ntrivcvgap0  12341  prodmodclem3  12367  prodmodclem2a  12368  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  fprodmul  12383  prodsnf  12384  absdvdsb  12601  zdvdsdc  12604  dvdsabseq  12639  dvdsdivcl  12642  dvdsext  12647  divalglemnn  12710  divalglemeunn  12713  divalglemeuneg  12715  divalgmod  12719  ndvdssub  12722  gcdsupex  12759  gcdsupcl  12760  gcddvds  12765  dvdslegcd  12766  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemmo  12808  bezoutlemeu  12809  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dfgcd2  12816  gcdzeq  12824  dvdssq  12833  nnwodc  12838  uzwodc  12839  nnwofdc  12840  nn0seqcvgd  12844  algcvgblem  12852  lcmval  12866  lcmdvds  12882  lcmgcdeq  12886  coprmgcdb  12891  ncoprmgcdne1b  12892  coprmdvds1  12894  1nprm  12917  1idssfct  12918  isprm2lem  12919  isprm2  12920  dvdsprime  12925  nprm  12926  3prm  12931  dvdsprm  12941  exprmfct  12942  isprm5lem  12945  isprm5  12946  coprm  12948  sqrt2irr  12966  dvdsfi  13046  phisum  13048  odzval  13049  pythagtriplem4  13076  pc2dvds  13138  pcprmpw2  13141  pcprmpw  13142  dvdsprmpweqle  13145  oddprmdvds  13162  prmpwdvds  13163  pockthg  13165  1arith  13175  prmlem0  13249  prmlem1a  13250  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsv  13311  ballotfilemsf1o  13315  ballotfi  13340  exmidunben  13375  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  imasaddfnlemg  13694  ringunitsap0  14703  drnguiap  14718  cnfldui  15033  znleval  15097  psrbagconcl  15173  gsumbagdiaglem  15175  rhmpsrfilem2  15185  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  ssblex  15657  comet  15725  bdmopn  15730  reopnap  15772  divcnap  15791  cdivcncfap  15830  cnopnap  15837  divcncfap  15840  maxcncf  15841  mincncf  15842  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeulemeu  15848  dedekindeu  15849  suplociccreex  15850  dedekindicclemuub  15852  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemeu  15857  dedekindicclemicc  15858  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthinc  15869  ivthreinc  15871  dich0  15878  ivthdich  15879  limcdifap  15888  limcimolemlt  15890  limccoap  15904  dvlemap  15906  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  dveflem  15952  logltb  16104  2irrexpqap  16214  prmdvdsfi  16243  sgmnncl  16257  dvdsppwf1o  16283  mpodvdsmulf1o  16284  perfectlem2  16300  bcmono  16304  bpos1lem  16309  bposlem9  16319  lgsmod  16350  lgsne0  16362  gausslemma2dlem4  16388  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  upgrm  16546  upgr1or2  16547  umgredg2en  16555  umgrbien  16556  upgr1elem1  16566  umgr1een  16571  edgupgren  16587  edgumgren  16588  umgredgnlp  16598  edgusgren  16609  usgruspgrben  16632  usgr1e  16687  subumgredg2en  16717  subupgr  16719  wlkvtxiedg  16791  wlkvtxiedgg  16792  istrl  16831  iseupth  16893  eupth2fi  16925  konigsberglem1  16934  lealltlt1  16956  pw1nct  17238  sbthom  17277  rirrdisj  17291  trilpo  17299  trirec0  17300  reap0  17315  cndcap  17316  dcapnconst  17318  neapmkv  17325  neap0mkv  17326  ltlenmkv  17327