Theorem breq12d 4047

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   class class class wbr 4034

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  breq123d  4048  3brtr3d  4065  3brtr4d  4066  pocl  4339  csbcnvg  4851  cnvpom  5213  sbcfung  5283  isoeq1  5851  isocnv  5861  isotr  5866  caovordig  6093  caovordg  6095  caovord2d  6097  caovord  6099  ofrfval  6148  ofrval  6150  ofrfval2  6156  caofref  6164  fundmeng  6875  xpsneng  6890  xpcomeng  6896  xpdom2g  6900  phplem3g  6926  php5  6928  php5dom  6933  exmidpw2en  6982  exmidapne  7345  nqtri3or  7482  ltsonq  7484  ltanqg  7486  ltmnqg  7487  lt2addnq  7490  lt2mulnq  7491  prarloclemarch  7504  ltrnqg  7506  ltnnnq  7509  prarloclemlt  7579  addlocprlemgt  7620  mullocprlem  7656  addextpr  7707  recexprlemss1l  7721  recexprlemss1u  7722  recexpr  7724  caucvgprlemcanl  7730  cauappcvgprlemm  7731  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlemlim  7747  cauappcvgpr  7748  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgpr  7768  caucvgprprlemell  7771  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemnkeqj  7776  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemloc  7789  caucvgprprlemclphr  7791  caucvgprprlemexb  7793  caucvgprprlem1  7795  lttrsr  7848  ltposr  7849  ltsosr  7850  ltasrg  7856  aptisr  7865  mulextsr1lem  7866  mulextsr1  7867  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  caucvgsr  7888  axpre-ltirr  7968  axpre-ltadd  7972  axpre-mulgt0  7973  axpre-mulext  7974  axcaucvglemcau  7984  axcaucvglemres  7985  ltadd2  8465  ltadd1  8475  leadd2  8477  reapval  8622  reapmul1  8641  remulext2  8646  apreim  8649  apirr  8651  apsym  8652  apcotr  8653  apadd1  8654  apadd2  8655  apneg  8657  mulext1  8658  mulext2  8659  apti  8668  apsub1  8688  subap0  8689  apmul1  8834  apmul2  8835  apdivmuld  8859  ltmul2  8902  lemul2  8903  ltdiv1  8914  ltdiv2  8933  ledivdiv  8936  lediv2  8937  negiso  9001  div4p1lem1div2  9264  qapne  9732  nn0ledivnn  9861  xleadd1  9969  xltadd1  9970  xltadd2  9971  xsubge0  9975  xleaddadd  9981  qtri3or  10349  frecfzennn  10537  monoord  10596  monoord2  10597  leexp1a  10705  bernneq  10771  apexp1  10829  nn0le2msqd  10830  faclbnd  10852  faclbnd3  10854  faclbnd6  10855  facubnd  10856  fihashdom  10914  zfz1isolemiso  10950  cjap  11090  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemlo  11197  resqrexlemcalc3  11200  absext  11247  xrnegiso  11446  xrminltinf  11456  fsumabs  11649  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  fprodle  11824  addmodlteqALT  12043  nn0seqcvgd  12236  algcvg  12243  algcvga  12246  eucalgcvga  12253  qnumgt0  12393  pcprendvds2  12487  pcpremul  12489  pcadd2  12537  2expltfac  12635  ctinfomlemom  12671  gsumfzval  13095  mplsubgfilemcl  14333  ispsmet  14667  psmettri2  14672  ismet  14688  isxmet  14689  xmettri2  14705  blvalps  14732  blval  14733  comet  14843  bdxmet  14845  dvef  15071  cxplt  15260  rpcxple2  15262  rpcxplt2  15263  cxplt3  15264  apcxp2  15283  ltexp2  15285  logbleb  15305  logblt  15306  lgsdilem  15376  2lgslem1a2  15436  apdifflemr  15804  apdiff  15805