Theorem breq1 4048

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2176  ⟨cop 3636   class class class wbr 4045

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046

This theorem is referenced by:  breq12  4050  breq1i  4052  breq1d  4055  nbrne2  4065  brab1  4092  pocl  4351  swopolem  4353  swopo  4354  issod  4367  sowlin  4368  sotritrieq  4373  frirrg  4398  wetriext  4626  vtoclr  4724  brcog  4846  brcogw  4848  opelcnvg  4859  dfdmf  4872  eldmg  4874  dfrnf  4920  dfres2  5012  imasng  5048  coi1  5199  dffun6f  5285  funmo  5287  fun11  5342  fveq2  5578  funfveu  5591  sefvex  5599  nfunsn  5613  fvmptss2  5656  f1ompt  5733  fmptco  5748  dff13  5839  foeqcnvco  5861  isorel  5879  isocnv  5882  isotr  5887  isoini  5889  isopolem  5893  isosolem  5895  f1oiso  5897  f1oiso2  5898  caovordig  6114  caovordg  6116  caovord3d  6119  caovord  6120  caovord3  6122  caofrss  6192  caoftrn  6193  poxp  6320  brtpos2  6339  rntpos  6345  tpostpos  6352  ertr  6637  ecopovsym  6720  ecopovtrn  6721  ecopovsymg  6723  ecopovtrng  6724  th3qlem2  6727  isfi  6854  en0  6889  en1  6893  en1bg  6894  endisj  6921  xpcomco  6923  dom0  6937  ssenen  6950  nneneq  6956  domfiexmid  6977  findcard  6987  findcard2  6988  findcard2s  6989  isinfinf  6996  tridc  6998  fimax2gtrilemstep  6999  fimax2gtri  7000  fiintim  7030  fisseneq  7033  en1eqsnbi  7053  isbth  7071  supmoti  7097  eqsupti  7100  supubti  7103  suplubti  7104  supsnti  7109  isotilem  7110  isoti  7111  supisolem  7112  supisoex  7113  infminti  7131  isnumi  7291  cardval3ex  7294  oncardval  7295  cardonle  7296  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidapne  7374  nqtri3or  7511  ltsonq  7513  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  subhalfnqq  7529  ltbtwnnqq  7530  archnqq  7532  nqnq0pi  7553  prcdnql  7599  prcunqu  7600  prnmaxl  7603  genpcuu  7635  genprndl  7636  genprndu  7637  nqprm  7657  nqprrnd  7658  nqprdisj  7659  nqprloc  7660  nqpru  7667  addnqprlemrl  7672  addnqprlemfl  7674  addnqprlemfu  7675  prmuloc2  7682  mulnqprlemrl  7688  mulnqprlemfl  7690  mulnqprlemfu  7691  1idprl  7705  ltnqpr  7708  ltnqpri  7709  prplnqu  7735  recexprlemell  7737  recexprlemm  7739  recexprlemdisj  7745  recexprlemloc  7746  recexprlem1ssu  7749  recexprlemss1l  7750  aptiprlemu  7755  archpr  7758  cauappcvgprlemm  7760  cauappcvgprlemladdfl  7770  cauappcvgprlem2  7775  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemcl  7791  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemelu  7801  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemnbj  7808  caucvgprprlemmu  7810  caucvgprprlemopu  7814  caucvgprprlemexbt  7821  caucvgprprlemaddq  7823  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgprpr  7827  suplocexprlemmu  7833  suplocexprlemloc  7836  suplocexpr  7840  lttrsr  7877  ltsosr  7879  1ne0sr  7881  ltasrg  7885  aptisr  7894  mulextsr1  7896  archsr  7897  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axpre-ltwlin  7998  axpre-lttrn  7999  axpre-apti  8000  axpre-ltadd  8001  axpre-mulext  8003  axcaucvglemcau  8013  axcaucvglemres  8014  axcaucvg  8015  axpre-suploclemres  8016  axpre-suploc  8017  ltxrlt  8140  lttri3  8154  ltordlem  8557  lt0ne0d  8588  reapti  8654  apreim  8678  apsscn  8722  recexap  8728  lbreu  9020  lble  9022  suprleubex  9029  sup3exmid  9032  nnsub  9077  nominpos  9277  nn0n0n1ge2b  9454  zextle  9466  fzind  9490  btwnz  9494  uzval  9652  supinfneg  9718  infsupneg  9719  infregelbex  9721  ublbneg  9736  lbzbi  9739  qreccl  9765  xrltnsym  9917  xrlttr  9919  xrltso  9920  xrlttri3  9921  nltpnft  9938  npnflt  9939  xrrebnd  9943  xltnegi  9959  xnn0lenn0nn0  9989  xsubge0  10005  xlesubadd  10007  xleaddadd  10011  ixxval  10020  elixx1  10021  elioo2  10045  iccid  10049  fzval  10134  elfz1  10137  zsupcllemstep  10374  suprzubdc  10381  zsupssdc  10383  qtri3or  10385  exbtwnzlemstep  10392  exbtwnzlemshrink  10393  exbtwnzlemex  10394  exbtwnz  10395  rebtwn2zlemstep  10397  rebtwn2zlemshrink  10398  rebtwn2z  10399  qbtwnre  10401  qbtwnxr  10402  flval  10417  flqlelt  10421  flqbi  10435  flqeqceilz  10465  modqid2  10498  seq3f1olemqsum  10660  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem2  10667  expcl2lemap  10698  expclzaplem  10710  expclzap  10711  expap0i  10718  nn0ltexp2  10856  hashinfuni  10924  hashennnuni  10926  hashunlem  10951  zfz1isolemiso  10986  zfz1isolem1  10987  zfz1iso  10988  absle  11433  maxleast  11557  rexanre  11564  rexico  11565  fimaxre2  11571  minmax  11574  xrmaxltsup  11602  xrminmax  11609  climshft  11648  reccn2ap  11657  summodclem3  11724  summodclem2a  11725  summodc  11727  zsumdc  11728  fsum3  11731  fsum3cvg3  11740  fsumcl2lem  11742  fsumadd  11750  sumsnf  11753  fsummulc2  11792  isumlessdc  11840  cvgratz  11876  mertenslemi1  11879  ntrivcvgap0  11893  prodmodclem3  11919  prodmodclem2a  11920  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  fprodmul  11935  prodsnf  11936  absdvdsb  12153  zdvdsdc  12156  dvdsabseq  12191  dvdsdivcl  12194  dvdsext  12199  divalglemnn  12262  divalglemeunn  12265  divalglemeuneg  12267  divalgmod  12271  ndvdssub  12274  gcdsupex  12311  gcdsupcl  12312  gcddvds  12317  dvdslegcd  12318  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemzz  12356  bezoutlemmo  12360  bezoutlemeu  12361  bezoutlemle  12362  bezoutlemsup  12363  dfgcd3  12364  dfgcd2  12368  gcdzeq  12376  dvdssq  12385  nnwodc  12390  uzwodc  12391  nnwofdc  12392  nn0seqcvgd  12396  algcvgblem  12404  lcmval  12418  lcmdvds  12434  lcmgcdeq  12438  coprmgcdb  12443  ncoprmgcdne1b  12444  coprmdvds1  12446  1nprm  12469  1idssfct  12470  isprm2lem  12471  isprm2  12472  dvdsprime  12477  nprm  12478  3prm  12483  dvdsprm  12492  exprmfct  12493  isprm5lem  12496  isprm5  12497  coprm  12499  sqrt2irr  12517  dvdsfi  12594  phisum  12596  odzval  12597  pythagtriplem4  12624  pc2dvds  12686  pcprmpw2  12689  pcprmpw  12690  dvdsprmpweqle  12693  oddprmdvds  12710  prmpwdvds  12711  pockthg  12713  1arith  12723  exmidunben  12830  nninfdclemcl  12852  nninfdclemp1  12854  nninfdc  12857  imasaddfnlemg  13179  cnfldui  14384  znleval  14448  ssblex  14936  comet  15004  bdmopn  15009  reopnap  15051  divcnap  15070  cdivcncfap  15109  cnopnap  15116  divcncfap  15119  maxcncf  15120  mincncf  15121  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  dedekindeulemeu  15127  dedekindeu  15128  suplociccreex  15129  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  dedekindicclemeu  15136  dedekindicclemicc  15137  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemloc  15146  ivthinc  15148  ivthreinc  15150  dich0  15157  ivthdich  15158  limcdifap  15167  limcimolemlt  15169  limccoap  15183  dvlemap  15185  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvcnp2cntop  15204  dvaddxxbr  15206  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvrecap  15218  dveflem  15231  logltb  15379  2irrexpqap  15483  sgmnncl  15493  dvdsppwf1o  15494  mpodvdsmulf1o  15495  perfectlem2  15505  lgsmod  15536  lgsne0  15548  gausslemma2dlem4  15574  2sqlem6  15630  2sqlem8  15633  2sqlem10  15635  pw1nct  15977  sbthom  16002  trilpo  16019  trirec0  16020  reap0  16034  cndcap  16035  dcapnconst  16037  neapmkv  16044  neap0mkv  16045  ltlenmkv  16046