Theorem breq1 3940

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ⟨cop 3535   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  breq12  3942  breq1i  3944  breq1d  3947  nbrne2  3956  brab1  3983  pocl  4233  swopolem  4235  swopo  4236  issod  4249  sowlin  4250  sotritrieq  4255  frirrg  4280  wetriext  4499  vtoclr  4595  brcog  4714  brcogw  4716  opelcnvg  4727  dfdmf  4740  eldmg  4742  dfrnf  4788  dfres2  4879  imasng  4912  coi1  5062  dffun6f  5144  funmo  5146  fun11  5198  fveq2  5429  funfveu  5442  sefvex  5450  nfunsn  5463  fvmptss2  5504  f1ompt  5579  fmptco  5594  dff13  5677  foeqcnvco  5699  isorel  5717  isocnv  5720  isotr  5725  isoini  5727  isopolem  5731  isosolem  5733  f1oiso  5735  f1oiso2  5736  caovordig  5944  caovordg  5946  caovord3d  5949  caovord  5950  caovord3  5952  caofrss  6014  caoftrn  6015  poxp  6137  brtpos2  6156  rntpos  6162  tpostpos  6169  ertr  6452  ecopovsym  6533  ecopovtrn  6534  ecopovsymg  6536  ecopovtrng  6537  th3qlem2  6540  isfi  6663  en0  6697  en1  6701  en1bg  6702  endisj  6726  xpcomco  6728  dom0  6740  ssenen  6753  nneneq  6759  domfiexmid  6780  findcard  6790  findcard2  6791  findcard2s  6792  isinfinf  6799  tridc  6801  fimax2gtrilemstep  6802  fimax2gtri  6803  fiintim  6825  fisseneq  6828  en1eqsnbi  6845  isbth  6863  supmoti  6888  eqsupti  6891  supubti  6894  suplubti  6895  supsnti  6900  isotilem  6901  isoti  6902  supisolem  6903  supisoex  6904  infminti  6922  isnumi  7055  cardval3ex  7058  oncardval  7059  cardonle  7060  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  nqtri3or  7228  ltsonq  7230  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  subhalfnqq  7246  ltbtwnnqq  7247  archnqq  7249  nqnq0pi  7270  prcdnql  7316  prcunqu  7317  prnmaxl  7320  genpcuu  7352  genprndl  7353  genprndu  7354  nqprm  7374  nqprrnd  7375  nqprdisj  7376  nqprloc  7377  nqpru  7384  addnqprlemrl  7389  addnqprlemfl  7391  addnqprlemfu  7392  prmuloc2  7399  mulnqprlemrl  7405  mulnqprlemfl  7407  mulnqprlemfu  7408  1idprl  7422  ltnqpr  7425  ltnqpri  7426  prplnqu  7452  recexprlemell  7454  recexprlemm  7456  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssu  7466  recexprlemss1l  7467  aptiprlemu  7472  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemladdfl  7487  cauappcvgprlem2  7492  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemcl  7508  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnbj  7525  caucvgprprlemmu  7527  caucvgprprlemopu  7531  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  caucvgprprlem1  7541  caucvgprprlem2  7542  caucvgprpr  7544  suplocexprlemmu  7550  suplocexprlemloc  7553  suplocexpr  7557  lttrsr  7594  ltsosr  7596  1ne0sr  7598  ltasrg  7602  aptisr  7611  mulextsr1  7613  archsr  7614  caucvgsrlemgt1  7627  caucvgsrlemoffres  7632  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axpre-ltwlin  7715  axpre-lttrn  7716  axpre-apti  7717  axpre-ltadd  7718  axpre-mulext  7720  axcaucvglemcau  7730  axcaucvglemres  7731  axcaucvg  7732  axpre-suploclemres  7733  axpre-suploc  7734  ltxrlt  7854  lttri3  7868  ltordlem  8268  lt0ne0d  8299  reapti  8365  apreim  8389  apsscn  8433  recexap  8438  lbreu  8727  lble  8729  suprleubex  8736  sup3exmid  8739  nnsub  8783  nominpos  8981  nn0n0n1ge2b  9154  zextle  9166  fzind  9190  btwnz  9194  uzval  9352  supinfneg  9417  infsupneg  9418  ublbneg  9432  lbzbi  9435  qreccl  9461  xrltnsym  9609  xrlttr  9611  xrltso  9612  xrlttri3  9613  nltpnft  9627  npnflt  9628  xrrebnd  9632  xltnegi  9648  xnn0lenn0nn0  9678  xsubge0  9694  xlesubadd  9696  xleaddadd  9700  ixxval  9709  elixx1  9710  elioo2  9734  iccid  9738  fzval  9823  elfz1  9826  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemshrink  10057  exbtwnzlemex  10058  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2zlemshrink  10062  rebtwn2z  10063  qbtwnre  10065  qbtwnxr  10066  flval  10076  flqlelt  10080  flqbi  10094  flqeqceilz  10122  modqid2  10155  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  expcl2lemap  10336  expclzaplem  10348  expclzap  10349  expap0i  10356  hashinfuni  10555  hashennnuni  10557  hashunlem  10582  zfz1isolemiso  10614  zfz1isolem1  10615  zfz1iso  10616  absle  10893  maxleast  11017  rexanre  11024  rexico  11025  fimaxre2  11030  minmax  11033  xrmaxltsup  11059  xrminmax  11066  climshft  11105  reccn2ap  11114  summodclem3  11181  summodclem2a  11182  summodc  11184  zsumdc  11185  fsum3  11188  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  sumsnf  11210  fsummulc2  11249  isumlessdc  11297  cvgratz  11333  mertenslemi1  11336  ntrivcvgap0  11350  prodmodclem3  11376  prodmodclem2a  11377  prodmodc  11379  zproddc  11380  fprodseq  11384  absdvdsb  11547  zdvdsdc  11550  dvdsabseq  11581  dvdsdivcl  11584  dvdsext  11589  divalglemnn  11651  divalglemeunn  11654  divalglemeuneg  11656  divalgmod  11660  ndvdssub  11663  zsupcllemstep  11674  gcdsupex  11682  gcdsupcl  11683  gcddvds  11688  dvdslegcd  11689  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemmo  11730  bezoutlemeu  11731  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dfgcd2  11738  gcdzeq  11746  dvdssq  11755  nn0seqcvgd  11758  algcvgblem  11766  lcmval  11780  lcmdvds  11796  lcmgcdeq  11800  coprmgcdb  11805  ncoprmgcdne1b  11806  coprmdvds1  11808  1nprm  11831  1idssfct  11832  isprm2lem  11833  isprm2  11834  dvdsprime  11839  nprm  11840  3prm  11845  dvdsprm  11853  exprmfct  11854  coprm  11858  sqrt2irr  11876  exmidunben  11975  ssblex  12639  comet  12707  bdmopn  12712  reopnap  12746  divcnap  12763  cdivcncfap  12795  cnopnap  12802  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeulemeu  12808  dedekindeu  12809  suplociccreex  12810  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemeu  12817  dedekindicclemicc  12818  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limcdifap  12839  limcimolemlt  12841  limccoap  12855  dvlemap  12857  dvidlemap  12868  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  dveflem  12895  logltb  13003  2irrexpqap  13103  pw1nct  13371  sbthom  13396  trilpo  13411  trirec0  13412  neapmkv  13425