Theorem breq12d 4000

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breq12d	⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		breq12 3992	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 409	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   class class class wbr 3987

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  breq123d  4001  3brtr3d  4018  3brtr4d  4019  pocl  4286  csbcnvg  4793  cnvpom  5151  sbcfung  5220  isoeq1  5778  isocnv  5788  isotr  5793  caovordig  6016  caovordg  6018  caovord2d  6020  caovord  6022  ofrfval  6067  ofrval  6069  ofrfval2  6075  caofref  6080  fundmeng  6782  xpsneng  6797  xpcomeng  6803  xpdom2g  6807  phplem3g  6831  php5  6833  php5dom  6838  nqtri3or  7347  ltsonq  7349  ltanqg  7351  ltmnqg  7352  lt2addnq  7355  lt2mulnq  7356  prarloclemarch  7369  ltrnqg  7371  ltnnnq  7374  prarloclemlt  7444  addlocprlemgt  7485  mullocprlem  7521  addextpr  7572  recexprlemss1l  7586  recexprlemss1u  7587  recexpr  7589  caucvgprlemcanl  7595  cauappcvgprlemm  7596  cauappcvgprlemdisj  7602  cauappcvgprlemloc  7603  cauappcvgprlemladdru  7607  cauappcvgprlemladdrl  7608  cauappcvgprlem1  7610  cauappcvgprlemlim  7612  cauappcvgpr  7613  caucvgprlemnkj  7617  caucvgprlemnbj  7618  caucvgprlemdisj  7625  caucvgprlemloc  7626  caucvgprlemcl  7627  caucvgprlemladdrl  7629  caucvgprlem1  7630  caucvgpr  7633  caucvgprprlemell  7636  caucvgprprlemcbv  7638  caucvgprprlemval  7639  caucvgprprlemnkeqj  7641  caucvgprprlemopl  7648  caucvgprprlemlol  7649  caucvgprprlemloc  7654  caucvgprprlemclphr  7656  caucvgprprlemexb  7658  caucvgprprlem1  7660  lttrsr  7713  ltposr  7714  ltsosr  7715  ltasrg  7721  aptisr  7730  mulextsr1lem  7731  mulextsr1  7732  caucvgsrlemcau  7744  caucvgsrlemgt1  7746  caucvgsrlemoffcau  7749  caucvgsrlemoffres  7751  caucvgsr  7753  axpre-ltirr  7833  axpre-ltadd  7837  axpre-mulgt0  7838  axpre-mulext  7839  axcaucvglemcau  7849  axcaucvglemres  7850  ltadd2  8327  ltadd1  8337  leadd2  8339  reapval  8484  reapmul1  8503  remulext2  8508  apreim  8511  apirr  8513  apsym  8514  apcotr  8515  apadd1  8516  apadd2  8517  apneg  8519  mulext1  8520  mulext2  8521  apti  8530  apsub1  8550  subap0  8551  apmul1  8694  apmul2  8695  apdivmuld  8719  ltmul2  8761  lemul2  8762  ltdiv1  8773  ltdiv2  8792  ledivdiv  8795  lediv2  8796  negiso  8860  div4p1lem1div2  9120  qapne  9587  nn0ledivnn  9713  xleadd1  9821  xltadd1  9822  xltadd2  9823  xsubge0  9827  xleaddadd  9833  qtri3or  10188  frecfzennn  10371  monoord  10421  monoord2  10422  leexp1a  10520  bernneq  10585  apexp1  10641  nn0le2msqd  10642  faclbnd  10664  faclbnd3  10666  faclbnd6  10667  facubnd  10668  fihashdom  10727  zfz1isolemiso  10763  cjap  10859  cvg1nlemcau  10937  cvg1nlemres  10938  resqrexlemlo  10966  resqrexlemcalc3  10969  absext  11016  xrnegiso  11214  xrminltinf  11224  fsumabs  11417  cvgratnnlemnexp  11476  cvgratnnlemmn  11477  fprodle  11592  addmodlteqALT  11808  nn0seqcvgd  11984  algcvg  11991  algcvga  11994  eucalgcvga  12001  qnumgt0  12141  pcprendvds2  12234  pcpremul  12236  ctinfomlemom  12371  ispsmet  13078  psmettri2  13083  ismet  13099  isxmet  13100  xmettri2  13116  blvalps  13143  blval  13144  comet  13254  bdxmet  13256  dvef  13443  cxplt  13591  rpcxple2  13593  rpcxplt2  13594  cxplt3  13595  apcxp2  13613  ltexp2  13615  logbleb  13634  logblt  13635  lgsdilem  13683  apdifflemr  14041  apdiff  14042