Theorem breq1 4131

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ⟨cop 3711   class class class wbr 4128

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-br 4129

This theorem is referenced by:  breq12  4133  breq1i  4135  breq1d  4138  nbrne2  4148  brab1  4176  pocl  4446  swopolem  4448  swopo  4449  issod  4462  sowlin  4463  sotritrieq  4468  frirrg  4493  wetriext  4722  vtoclr  4821  brcog  4945  brcogw  4947  opelcnvg  4958  dfdmf  4972  eldmg  4974  dfrnf  5021  dfres2  5113  imasng  5150  coi1  5301  dffun6f  5388  funmo  5390  fun11  5446  fveq2  5693  funfveu  5706  sefvex  5714  nfunsn  5730  fvmptss2  5777  f1ompt  5853  fmptco  5868  dff13  5967  foeqcnvco  5989  isorel  6007  isocnv  6010  isotr  6015  isoini  6017  isopolem  6021  isosolem  6023  f1oiso  6025  f1oiso2  6026  caovordig  6248  caovordg  6250  caovord3d  6253  caovord  6254  caovord3  6256  caofrss  6327  caoftrn  6328  poxp  6461  brtpos2  6515  rntpos  6521  tpostpos  6528  ertr  6815  ecopovsym  6898  ecopovtrn  6899  ecopovsymg  6901  ecopovtrng  6902  th3qlem2  6905  isfi  7040  en0  7075  en1  7079  en1bg  7080  endisj  7115  xpcomco  7117  dom0  7131  ssenen  7145  nneneq  7151  domfiexmid  7175  findcard  7185  findcard2  7186  findcard2s  7187  isinfinf  7194  tridc  7197  fimax2gtrilemstep  7198  fimax2gtri  7199  fiintim  7231  fisseneq  7235  en1eqsnbi  7259  isbth  7277  supmoti  7326  eqsupti  7329  supubti  7332  suplubti  7333  supsnti  7338  isotilem  7339  isoti  7340  supisolem  7341  supisoex  7342  infminti  7360  isnumi  7520  cardval3ex  7523  oncardval  7524  cardonle  7525  en2prde  7532  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  papsym  7605  papcotr  7606  exmidapne  7619  nqtri3or  7756  ltsonq  7758  ltanqg  7760  ltmnqg  7761  ltexnqq  7768  subhalfnqq  7774  ltbtwnnqq  7775  archnqq  7777  nqnq0pi  7798  prcdnql  7844  prcunqu  7845  prnmaxl  7848  genpcuu  7880  genprndl  7881  genprndu  7882  nqprm  7902  nqprrnd  7903  nqprdisj  7904  nqprloc  7905  nqpru  7912  addnqprlemrl  7917  addnqprlemfl  7919  addnqprlemfu  7920  prmuloc2  7927  mulnqprlemrl  7933  mulnqprlemfl  7935  mulnqprlemfu  7936  1idprl  7950  ltnqpr  7953  ltnqpri  7954  prplnqu  7980  recexprlemell  7982  recexprlemm  7984  recexprlemdisj  7990  recexprlemloc  7991  recexprlem1ssu  7994  recexprlemss1l  7995  aptiprlemu  8000  archpr  8003  cauappcvgprlemm  8005  cauappcvgprlemladdfl  8015  cauappcvgprlem2  8020  cauappcvgpr  8022  caucvgprlemnkj  8026  caucvgprlemnbj  8027  caucvgprlemcl  8036  caucvgprlem2  8040  caucvgpr  8042  caucvgprprlemelu  8046  caucvgprprlemcbv  8047  caucvgprprlemval  8048  caucvgprprlemnbj  8053  caucvgprprlemmu  8055  caucvgprprlemopu  8059  caucvgprprlemexbt  8066  caucvgprprlemaddq  8068  caucvgprprlem1  8069  caucvgprprlem2  8070  caucvgprpr  8072  suplocexprlemmu  8078  suplocexprlemloc  8081  suplocexpr  8085  lttrsr  8122  ltsosr  8124  1ne0sr  8126  ltasrg  8130  aptisr  8139  mulextsr1  8141  archsr  8142  caucvgsrlemgt1  8155  caucvgsrlemoffres  8160  caucvgsr  8162  suplocsrlemb  8166  suplocsrlempr  8167  suplocsrlem  8168  axpre-ltwlin  8243  axpre-lttrn  8244  axpre-apti  8245  axpre-ltadd  8246  axpre-mulext  8248  axcaucvglemcau  8258  axcaucvglemres  8259  axcaucvg  8260  axpre-suploclemres  8261  axpre-suploc  8262  ltxrlt  8384  lttri3  8398  ltordlem  8803  lt0ne0d  8834  reapti  8900  apreim  8924  apsscn  8968  recexap  8974  lbreu  9268  lble  9270  suprleubex  9277  sup3exmid  9280  nnsub  9325  nominpos  9525  nn0n0n1ge2b  9707  zextle  9719  fzind  9743  btwnz  9747  uzval  9905  supinfneg  9977  infsupneg  9978  infregelbex  9980  ublbneg  9995  lbzbi  9998  qreccl  10024  xrltnsym  10177  xrlttr  10179  xrltso  10180  xrlttri3  10181  nltpnft  10198  npnflt  10199  xrrebnd  10203  xltnegi  10219  xnn0lenn0nn0  10249  xsubge0  10265  xlesubadd  10267  xleaddadd  10271  ixxval  10280  elixx1  10281  elioo2  10305  iccid  10309  fzval  10395  elfz1  10398  zsupcllemstep  10643  suprzubdc  10652  zsupssdc  10654  qtri3or  10656  exbtwnzlemstep  10663  exbtwnzlemshrink  10664  exbtwnzlemex  10665  exbtwnz  10666  rebtwn2zlemstep  10668  rebtwn2zlemshrink  10669  rebtwn2z  10670  qbtwnre  10672  qbtwnxr  10673  flval  10688  flqlelt  10692  flqbi  10706  flqeqceilz  10736  modqid2  10769  seq3f1olemqsum  10931  seq3f1oleml  10934  seq3f1o  10935  seqf1oglem2  10938  expcl2lemap  10969  expclzaplem  10981  expclzap  10982  expap0i  10989  nn0ltexp2  11128  hashinfuni  11197  hashennnuni  11199  hashunlem  11225  zfz1isolemiso  11272  zfz1isolem1  11273  zfz1iso  11274  absle  11836  maxleast  11960  rexanre  11967  rexico  11968  fimaxre2  11974  minmax  11977  xrmaxltsup  12005  xrminmax  12012  climshft  12051  reccn2ap  12060  summodclem3  12128  summodclem2a  12129  summodc  12131  zsumdc  12132  fsum3  12135  fsum3cvg3  12144  fsumcl2lem  12146  fsumadd  12154  sumsnf  12157  fsummulc2  12196  isumlessdc  12244  cvgratz  12280  mertenslemi1  12283  ntrivcvgap0  12297  prodmodclem3  12323  prodmodclem2a  12324  prodmodc  12326  zproddc  12327  fprodseq  12331  fprodntrivap  12332  fprodmul  12339  prodsnf  12340  absdvdsb  12557  zdvdsdc  12560  dvdsabseq  12595  dvdsdivcl  12598  dvdsext  12603  divalglemnn  12666  divalglemeunn  12669  divalglemeuneg  12671  divalgmod  12675  ndvdssub  12678  gcdsupex  12715  gcdsupcl  12716  gcddvds  12721  dvdslegcd  12722  bezoutlemmain  12756  bezoutlemex  12759  bezoutlemzz  12760  bezoutlemmo  12764  bezoutlemeu  12765  bezoutlemle  12766  bezoutlemsup  12767  dfgcd3  12768  dfgcd2  12772  gcdzeq  12780  dvdssq  12789  nnwodc  12794  uzwodc  12795  nnwofdc  12796  nn0seqcvgd  12800  algcvgblem  12808  lcmval  12822  lcmdvds  12838  lcmgcdeq  12842  coprmgcdb  12847  ncoprmgcdne1b  12848  coprmdvds1  12850  1nprm  12873  1idssfct  12874  isprm2lem  12875  isprm2  12876  dvdsprime  12881  nprm  12882  3prm  12887  dvdsprm  12896  exprmfct  12897  isprm5lem  12900  isprm5  12901  coprm  12903  sqrt2irr  12921  dvdsfi  12998  phisum  13000  odzval  13001  pythagtriplem4  13028  pc2dvds  13090  pcprmpw2  13093  pcprmpw  13094  dvdsprmpweqle  13097  oddprmdvds  13114  prmpwdvds  13115  pockthg  13117  1arith  13127  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemsv  13234  ballotfilemsf1o  13238  ballotfi  13263  exmidunben  13298  nninfdclemcl  13320  nninfdclemp1  13322  nninfdc  13325  imasaddfnlemg  13615  ringunitsap0  14570  drnguiap  14585  cnfldui  14899  znleval  14963  psrbagconcl  14989  ssblex  15458  comet  15526  bdmopn  15531  reopnap  15573  divcnap  15592  cdivcncfap  15631  cnopnap  15638  divcncfap  15641  maxcncf  15642  mincncf  15643  dedekindeulemuub  15644  dedekindeulemloc  15646  dedekindeulemlu  15648  dedekindeulemeu  15649  dedekindeu  15650  suplociccreex  15651  dedekindicclemuub  15653  dedekindicclemloc  15655  dedekindicclemlu  15657  dedekindicclemeu  15658  dedekindicclemicc  15659  dedekindicc  15660  ivthinclemlopn  15663  ivthinclemlr  15664  ivthinclemuopn  15665  ivthinclemur  15666  ivthinclemloc  15668  ivthinc  15670  ivthreinc  15672  dich0  15679  ivthdich  15680  limcdifap  15689  limcimolemlt  15691  limccoap  15705  dvlemap  15707  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvcnp2cntop  15726  dvaddxxbr  15728  dvmulxxbr  15729  dvcoapbr  15734  dvcjbr  15735  dvrecap  15740  dveflem  15753  logltb  15901  2irrexpqap  16006  sgmnncl  16019  dvdsppwf1o  16020  mpodvdsmulf1o  16021  perfectlem2  16031  lgsmod  16062  lgsne0  16074  gausslemma2dlem4  16100  2sqlem6  16156  2sqlem8  16159  2sqlem10  16161  upgrm  16258  upgr1or2  16259  umgredg2en  16267  umgrbien  16268  upgr1elem1  16278  umgr1een  16283  edgupgren  16299  edgumgren  16300  umgredgnlp  16310  edgusgren  16321  usgruspgrben  16344  usgr1e  16399  subumgredg2en  16429  subupgr  16431  wlkvtxiedg  16503  wlkvtxiedgg  16504  istrl  16543  iseupth  16605  eupth2fi  16637  konigsberglem1  16646  lealltlt1  16668  pw1nct  16950  sbthom  16979  trilpo  17000  trirec0  17001  reap0  17016  cndcap  17017  dcapnconst  17019  neapmkv  17026  neap0mkv  17027  ltlenmkv  17028