Theorem breq1 4047

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

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

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 4045

This theorem is referenced by:  breq12  4049  breq1i  4051  breq1d  4054  nbrne2  4064  brab1  4091  pocl  4350  swopolem  4352  swopo  4353  issod  4366  sowlin  4367  sotritrieq  4372  frirrg  4397  wetriext  4625  vtoclr  4723  brcog  4845  brcogw  4847  opelcnvg  4858  dfdmf  4871  eldmg  4873  dfrnf  4919  dfres2  5011  imasng  5047  coi1  5198  dffun6f  5284  funmo  5286  fun11  5341  fveq2  5576  funfveu  5589  sefvex  5597  nfunsn  5611  fvmptss2  5654  f1ompt  5731  fmptco  5746  dff13  5837  foeqcnvco  5859  isorel  5877  isocnv  5880  isotr  5885  isoini  5887  isopolem  5891  isosolem  5893  f1oiso  5895  f1oiso2  5896  caovordig  6112  caovordg  6114  caovord3d  6117  caovord  6118  caovord3  6120  caofrss  6190  caoftrn  6191  poxp  6318  brtpos2  6337  rntpos  6343  tpostpos  6350  ertr  6635  ecopovsym  6718  ecopovtrn  6719  ecopovsymg  6721  ecopovtrng  6722  th3qlem2  6725  isfi  6852  en0  6887  en1  6891  en1bg  6892  endisj  6919  xpcomco  6921  dom0  6935  ssenen  6948  nneneq  6954  domfiexmid  6975  findcard  6985  findcard2  6986  findcard2s  6987  isinfinf  6994  tridc  6996  fimax2gtrilemstep  6997  fimax2gtri  6998  fiintim  7028  fisseneq  7031  en1eqsnbi  7051  isbth  7069  supmoti  7095  eqsupti  7098  supubti  7101  suplubti  7102  supsnti  7107  isotilem  7108  isoti  7109  supisolem  7110  supisoex  7111  infminti  7129  isnumi  7289  cardval3ex  7292  oncardval  7293  cardonle  7294  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidapne  7372  nqtri3or  7509  ltsonq  7511  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  subhalfnqq  7527  ltbtwnnqq  7528  archnqq  7530  nqnq0pi  7551  prcdnql  7597  prcunqu  7598  prnmaxl  7601  genpcuu  7633  genprndl  7634  genprndu  7635  nqprm  7655  nqprrnd  7656  nqprdisj  7657  nqprloc  7658  nqpru  7665  addnqprlemrl  7670  addnqprlemfl  7672  addnqprlemfu  7673  prmuloc2  7680  mulnqprlemrl  7686  mulnqprlemfl  7688  mulnqprlemfu  7689  1idprl  7703  ltnqpr  7706  ltnqpri  7707  prplnqu  7733  recexprlemell  7735  recexprlemm  7737  recexprlemdisj  7743  recexprlemloc  7744  recexprlem1ssu  7747  recexprlemss1l  7748  aptiprlemu  7753  archpr  7756  cauappcvgprlemm  7758  cauappcvgprlemladdfl  7768  cauappcvgprlem2  7773  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemcl  7789  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnbj  7806  caucvgprprlemmu  7808  caucvgprprlemopu  7812  caucvgprprlemexbt  7819  caucvgprprlemaddq  7821  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgprpr  7825  suplocexprlemmu  7831  suplocexprlemloc  7834  suplocexpr  7838  lttrsr  7875  ltsosr  7877  1ne0sr  7879  ltasrg  7883  aptisr  7892  mulextsr1  7894  archsr  7895  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  caucvgsr  7915  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axpre-ltwlin  7996  axpre-lttrn  7997  axpre-apti  7998  axpre-ltadd  7999  axpre-mulext  8001  axcaucvglemcau  8011  axcaucvglemres  8012  axcaucvg  8013  axpre-suploclemres  8014  axpre-suploc  8015  ltxrlt  8138  lttri3  8152  ltordlem  8555  lt0ne0d  8586  reapti  8652  apreim  8676  apsscn  8720  recexap  8726  lbreu  9018  lble  9020  suprleubex  9027  sup3exmid  9030  nnsub  9075  nominpos  9275  nn0n0n1ge2b  9452  zextle  9464  fzind  9488  btwnz  9492  uzval  9650  supinfneg  9716  infsupneg  9717  infregelbex  9719  ublbneg  9734  lbzbi  9737  qreccl  9763  xrltnsym  9915  xrlttr  9917  xrltso  9918  xrlttri3  9919  nltpnft  9936  npnflt  9937  xrrebnd  9941  xltnegi  9957  xnn0lenn0nn0  9987  xsubge0  10003  xlesubadd  10005  xleaddadd  10009  ixxval  10018  elixx1  10019  elioo2  10043  iccid  10047  fzval  10132  elfz1  10135  zsupcllemstep  10372  suprzubdc  10379  zsupssdc  10381  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemshrink  10391  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2zlemshrink  10396  rebtwn2z  10397  qbtwnre  10399  qbtwnxr  10400  flval  10415  flqlelt  10419  flqbi  10433  flqeqceilz  10463  modqid2  10496  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem2  10665  expcl2lemap  10696  expclzaplem  10708  expclzap  10709  expap0i  10716  nn0ltexp2  10854  hashinfuni  10922  hashennnuni  10924  hashunlem  10949  zfz1isolemiso  10984  zfz1isolem1  10985  zfz1iso  10986  absle  11400  maxleast  11524  rexanre  11531  rexico  11532  fimaxre2  11538  minmax  11541  xrmaxltsup  11569  xrminmax  11576  climshft  11615  reccn2ap  11624  summodclem3  11691  summodclem2a  11692  summodc  11694  zsumdc  11695  fsum3  11698  fsum3cvg3  11707  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  fsummulc2  11759  isumlessdc  11807  cvgratz  11843  mertenslemi1  11846  ntrivcvgap0  11860  prodmodclem3  11886  prodmodclem2a  11887  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  fprodmul  11902  prodsnf  11903  absdvdsb  12120  zdvdsdc  12123  dvdsabseq  12158  dvdsdivcl  12161  dvdsext  12166  divalglemnn  12229  divalglemeunn  12232  divalglemeuneg  12234  divalgmod  12238  ndvdssub  12241  gcdsupex  12278  gcdsupcl  12279  gcddvds  12284  dvdslegcd  12285  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemzz  12323  bezoutlemmo  12327  bezoutlemeu  12328  bezoutlemle  12329  bezoutlemsup  12330  dfgcd3  12331  dfgcd2  12335  gcdzeq  12343  dvdssq  12352  nnwodc  12357  uzwodc  12358  nnwofdc  12359  nn0seqcvgd  12363  algcvgblem  12371  lcmval  12385  lcmdvds  12401  lcmgcdeq  12405  coprmgcdb  12410  ncoprmgcdne1b  12411  coprmdvds1  12413  1nprm  12436  1idssfct  12437  isprm2lem  12438  isprm2  12439  dvdsprime  12444  nprm  12445  3prm  12450  dvdsprm  12459  exprmfct  12460  isprm5lem  12463  isprm5  12464  coprm  12466  sqrt2irr  12484  dvdsfi  12561  phisum  12563  odzval  12564  pythagtriplem4  12591  pc2dvds  12653  pcprmpw2  12656  pcprmpw  12657  dvdsprmpweqle  12660  oddprmdvds  12677  prmpwdvds  12678  pockthg  12680  1arith  12690  exmidunben  12797  nninfdclemcl  12819  nninfdclemp1  12821  nninfdc  12824  imasaddfnlemg  13146  cnfldui  14351  znleval  14415  ssblex  14903  comet  14971  bdmopn  14976  reopnap  15018  divcnap  15037  cdivcncfap  15076  cnopnap  15083  divcncfap  15086  maxcncf  15087  mincncf  15088  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeulemeu  15094  dedekindeu  15095  suplociccreex  15096  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemeu  15103  dedekindicclemicc  15104  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthinc  15115  ivthreinc  15117  dich0  15124  ivthdich  15125  limcdifap  15134  limcimolemlt  15136  limccoap  15150  dvlemap  15152  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvrecap  15185  dveflem  15198  logltb  15346  2irrexpqap  15450  sgmnncl  15460  dvdsppwf1o  15461  mpodvdsmulf1o  15462  perfectlem2  15472  lgsmod  15503  lgsne0  15515  gausslemma2dlem4  15541  2sqlem6  15597  2sqlem8  15600  2sqlem10  15602  pw1nct  15940  sbthom  15965  trilpo  15982  trirec0  15983  reap0  15997  cndcap  15998  dcapnconst  16000  neapmkv  16007  neap0mkv  16008  ltlenmkv  16009