Theorem breq12d 4101

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 4093	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breq123d  4102  3brtr3d  4119  3brtr4d  4120  pocl  4400  csbcnvg  4914  cnvpom  5279  sbcfung  5350  isoeq1  5942  isocnv  5952  isotr  5957  caovordig  6188  caovordg  6190  caovord2d  6192  caovord  6194  ofrfval  6244  ofrval  6246  ofrfval2  6252  caofref  6260  fundmeng  6982  xpsneng  7006  xpcomeng  7012  xpdom2g  7016  phplem3g  7042  php5  7044  php5dom  7049  exmidpw2en  7104  exmidapne  7479  nqtri3or  7616  ltsonq  7618  ltanqg  7620  ltmnqg  7621  lt2addnq  7624  lt2mulnq  7625  prarloclemarch  7638  ltrnqg  7640  ltnnnq  7643  prarloclemlt  7713  addlocprlemgt  7754  mullocprlem  7790  addextpr  7841  recexprlemss1l  7855  recexprlemss1u  7856  recexpr  7858  caucvgprlemcanl  7864  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexb  7927  caucvgprprlem1  7929  lttrsr  7982  ltposr  7983  ltsosr  7984  ltasrg  7990  aptisr  7999  mulextsr1lem  8000  mulextsr1  8001  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  axpre-ltirr  8102  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  ltadd2  8599  ltadd1  8609  leadd2  8611  reapval  8756  reapmul1  8775  remulext2  8780  apreim  8783  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apadd2  8789  apneg  8791  mulext1  8792  mulext2  8793  apti  8802  apsub1  8822  subap0  8823  apmul1  8968  apmul2  8969  apdivmuld  8993  ltmul2  9036  lemul2  9037  ltdiv1  9048  ltdiv2  9067  ledivdiv  9070  lediv2  9071  negiso  9135  div4p1lem1div2  9398  qapne  9873  nn0ledivnn  10002  xleadd1  10110  xltadd1  10111  xltadd2  10112  xsubge0  10116  xleaddadd  10122  qtri3or  10501  frecfzennn  10689  monoord  10748  monoord2  10749  leexp1a  10857  bernneq  10923  apexp1  10981  nn0le2msqd  10982  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  facubnd  11008  fihashdom  11067  zfz1isolemiso  11104  cjap  11484  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemlo  11591  resqrexlemcalc3  11594  absext  11641  xrnegiso  11840  xrminltinf  11850  fsumabs  12044  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  fprodle  12219  addmodlteqALT  12438  nn0seqcvgd  12631  algcvg  12638  algcvga  12641  eucalgcvga  12648  qnumgt0  12788  pcprendvds2  12882  pcpremul  12884  pcadd2  12932  2expltfac  13030  ctinfomlemom  13066  gsumfzval  13492  mplsubgfilemcl  14732  ispsmet  15066  psmettri2  15071  ismet  15087  isxmet  15088  xmettri2  15104  blvalps  15131  blval  15132  comet  15242  bdxmet  15244  dvef  15470  cxplt  15659  rpcxple2  15661  rpcxplt2  15662  cxplt3  15663  apcxp2  15682  ltexp2  15684  logbleb  15704  logblt  15705  lgsdilem  15775  2lgslem1a2  15835  apdifflemr  16702  apdiff  16703