Theorem breq1 4117

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205  ⟨cop 3697   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  breq12  4119  breq1i  4121  breq1d  4124  nbrne2  4134  brab1  4162  pocl  4429  swopolem  4431  swopo  4432  issod  4445  sowlin  4446  sotritrieq  4451  frirrg  4476  wetriext  4704  vtoclr  4803  brcog  4927  brcogw  4929  opelcnvg  4940  dfdmf  4954  eldmg  4956  dfrnf  5003  dfres2  5095  imasng  5132  coi1  5283  dffun6f  5370  funmo  5372  fun11  5428  fveq2  5675  funfveu  5688  sefvex  5696  nfunsn  5712  fvmptss2  5757  f1ompt  5833  fmptco  5848  dff13  5947  foeqcnvco  5969  isorel  5987  isocnv  5990  isotr  5995  isoini  5997  isopolem  6001  isosolem  6003  f1oiso  6005  f1oiso2  6006  caovordig  6228  caovordg  6230  caovord3d  6233  caovord  6234  caovord3  6236  caofrss  6307  caoftrn  6308  poxp  6441  brtpos2  6495  rntpos  6501  tpostpos  6508  ertr  6795  ecopovsym  6878  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  th3qlem2  6885  isfi  7013  en0  7048  en1  7052  en1bg  7053  endisj  7088  xpcomco  7090  dom0  7104  ssenen  7118  nneneq  7124  domfiexmid  7148  findcard  7158  findcard2  7159  findcard2s  7160  isinfinf  7167  tridc  7170  fimax2gtrilemstep  7171  fimax2gtri  7172  fiintim  7204  fisseneq  7208  en1eqsnbi  7232  isbth  7250  supmoti  7297  eqsupti  7300  supubti  7303  suplubti  7304  supsnti  7309  isotilem  7310  isoti  7311  supisolem  7312  supisoex  7313  infminti  7331  isnumi  7491  cardval3ex  7494  oncardval  7495  cardonle  7496  en2prde  7503  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  papsym  7576  papcotr  7577  exmidapne  7590  nqtri3or  7727  ltsonq  7729  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  subhalfnqq  7745  ltbtwnnqq  7746  archnqq  7748  nqnq0pi  7769  prcdnql  7815  prcunqu  7816  prnmaxl  7819  genpcuu  7851  genprndl  7852  genprndu  7853  nqprm  7873  nqprrnd  7874  nqprdisj  7875  nqprloc  7876  nqpru  7883  addnqprlemrl  7888  addnqprlemfl  7890  addnqprlemfu  7891  prmuloc2  7898  mulnqprlemrl  7904  mulnqprlemfl  7906  mulnqprlemfu  7907  1idprl  7921  ltnqpr  7924  ltnqpri  7925  prplnqu  7951  recexprlemell  7953  recexprlemm  7955  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssu  7965  recexprlemss1l  7966  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemladdfl  7986  cauappcvgprlem2  7991  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemcl  8007  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgprpr  8043  suplocexprlemmu  8049  suplocexprlemloc  8052  suplocexpr  8056  lttrsr  8093  ltsosr  8095  1ne0sr  8097  ltasrg  8101  aptisr  8110  mulextsr1  8112  archsr  8113  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axpre-ltwlin  8214  axpre-lttrn  8215  axpre-apti  8216  axpre-ltadd  8217  axpre-mulext  8219  axcaucvglemcau  8229  axcaucvglemres  8230  axcaucvg  8231  axpre-suploclemres  8232  axpre-suploc  8233  ltxrlt  8355  lttri3  8369  ltordlem  8773  lt0ne0d  8804  reapti  8870  apreim  8894  apsscn  8938  recexap  8944  lbreu  9236  lble  9238  suprleubex  9245  sup3exmid  9248  nnsub  9293  nominpos  9493  nn0n0n1ge2b  9675  zextle  9687  fzind  9711  btwnz  9715  uzval  9873  supinfneg  9945  infsupneg  9946  infregelbex  9948  ublbneg  9963  lbzbi  9966  qreccl  9992  xrltnsym  10145  xrlttr  10147  xrltso  10148  xrlttri3  10149  nltpnft  10166  npnflt  10167  xrrebnd  10171  xltnegi  10187  xnn0lenn0nn0  10217  xsubge0  10233  xlesubadd  10235  xleaddadd  10239  ixxval  10248  elixx1  10249  elioo2  10273  iccid  10277  fzval  10363  elfz1  10366  zsupcllemstep  10611  suprzubdc  10620  zsupssdc  10622  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemshrink  10632  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2zlemshrink  10637  rebtwn2z  10638  qbtwnre  10640  qbtwnxr  10641  flval  10656  flqlelt  10660  flqbi  10674  flqeqceilz  10704  modqid2  10737  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem2  10906  expcl2lemap  10937  expclzaplem  10949  expclzap  10950  expap0i  10957  nn0ltexp2  11096  hashinfuni  11165  hashennnuni  11167  hashunlem  11193  zfz1isolemiso  11236  zfz1isolem1  11237  zfz1iso  11238  absle  11799  maxleast  11923  rexanre  11930  rexico  11931  fimaxre2  11937  minmax  11940  xrmaxltsup  11968  xrminmax  11975  climshft  12014  reccn2ap  12023  summodclem3  12091  summodclem2a  12092  summodc  12094  zsumdc  12095  fsum3  12098  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  sumsnf  12120  fsummulc2  12159  isumlessdc  12207  cvgratz  12243  mertenslemi1  12246  ntrivcvgap0  12260  prodmodclem3  12286  prodmodclem2a  12287  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  fprodmul  12302  prodsnf  12303  absdvdsb  12520  zdvdsdc  12523  dvdsabseq  12558  dvdsdivcl  12561  dvdsext  12566  divalglemnn  12629  divalglemeunn  12632  divalglemeuneg  12634  divalgmod  12638  ndvdssub  12641  gcdsupex  12678  gcdsupcl  12679  gcddvds  12684  dvdslegcd  12685  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemmo  12727  bezoutlemeu  12728  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  dfgcd2  12735  gcdzeq  12743  dvdssq  12752  nnwodc  12757  uzwodc  12758  nnwofdc  12759  nn0seqcvgd  12763  algcvgblem  12771  lcmval  12785  lcmdvds  12801  lcmgcdeq  12805  coprmgcdb  12810  ncoprmgcdne1b  12811  coprmdvds1  12813  1nprm  12836  1idssfct  12837  isprm2lem  12838  isprm2  12839  dvdsprime  12844  nprm  12845  3prm  12850  dvdsprm  12859  exprmfct  12860  isprm5lem  12863  isprm5  12864  coprm  12866  sqrt2irr  12884  dvdsfi  12961  phisum  12963  odzval  12964  pythagtriplem4  12991  pc2dvds  13053  pcprmpw2  13056  pcprmpw  13057  dvdsprmpweqle  13060  oddprmdvds  13077  prmpwdvds  13078  pockthg  13080  1arith  13090  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsv  13197  ballotfilemsf1o  13201  ballotfi  13226  exmidunben  13261  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  imasaddfnlemg  13578  ringunitsap0  14532  drnguiap  14547  cnfldui  14863  znleval  14927  psrbagconcl  14953  ssblex  15422  comet  15490  bdmopn  15495  reopnap  15537  divcnap  15556  cdivcncfap  15595  cnopnap  15602  divcncfap  15605  maxcncf  15606  mincncf  15607  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeulemeu  15613  dedekindeu  15614  suplociccreex  15615  dedekindicclemuub  15617  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicclemeu  15622  dedekindicclemicc  15623  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthinc  15634  ivthreinc  15636  dich0  15643  ivthdich  15644  limcdifap  15653  limcimolemlt  15655  limccoap  15669  dvlemap  15671  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dveflem  15717  logltb  15865  2irrexpqap  15969  sgmnncl  15982  dvdsppwf1o  15983  mpodvdsmulf1o  15984  perfectlem2  15994  lgsmod  16025  lgsne0  16037  gausslemma2dlem4  16063  2sqlem6  16119  2sqlem8  16122  2sqlem10  16124  upgrm  16221  upgr1or2  16222  umgredg2en  16230  umgrbien  16231  upgr1elem1  16241  umgr1een  16246  edgupgren  16262  edgumgren  16263  umgredgnlp  16273  edgusgren  16284  usgruspgrben  16307  usgr1e  16362  subumgredg2en  16392  subupgr  16394  wlkvtxiedg  16466  wlkvtxiedgg  16467  istrl  16506  iseupth  16568  eupth2fi  16600  konigsberglem1  16609  pw1nct  16903  sbthom  16932  trilpo  16953  trirec0  16954  reap0  16969  cndcap  16970  trimul0or  16971  dcapnconst  16973  neapmkv  16980  neap0mkv  16981  ltlenmkv  16982