Theorem breq12d 4143

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq123d  4144  3brtr3d  4161  3brtr4d  4162  pocl  4448  csbcnvg  4964  cnvpom  5330  sbcfung  5401  isoeq1  6007  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord2d  6259  caovord  6261  ofrfval  6311  ofrval  6313  ofrfval2  6319  caofref  6327  fundmeng  7095  xpsneng  7120  xpcomeng  7126  xpdom2g  7130  phplem3g  7157  php5  7159  php5dom  7164  exmidpw2en  7219  papirr  7611  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  lt2addnq  7771  lt2mulnq  7772  prarloclemarch  7785  ltrnqg  7787  ltnnnq  7790  prarloclemlt  7860  addlocprlemgt  7901  mullocprlem  7937  addextpr  7988  recexprlemss1l  8002  recexprlemss1u  8003  recexpr  8005  caucvgprlemcanl  8011  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexb  8074  caucvgprprlem1  8076  lttrsr  8129  ltposr  8130  ltsosr  8131  ltasrg  8137  aptisr  8146  mulextsr1lem  8147  mulextsr1  8148  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  axpre-ltirr  8249  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  ltadd2  8747  ltadd1  8757  leadd2  8759  reapval  8904  reapmul1  8923  remulext2  8928  apreim  8931  apirr  8933  apsym  8934  apcotr  8935  apadd1  8936  apadd2  8937  apneg  8939  mulext1  8940  mulext2  8941  apti  8950  apsub1  8970  subap0  8971  apmul1  9118  apmul2  9119  apdivmuld  9143  ltmul2  9186  lemul2  9187  ltdiv1  9198  ltdiv2  9217  ledivdiv  9220  lediv2  9221  negiso  9285  div4p1lem1div2  9559  qapne  10039  nn0ledivnn  10168  xleadd1  10277  xltadd1  10278  xltadd2  10279  xsubge0  10283  xleaddadd  10289  qtri3or  10675  frecfzennn  10863  monoord  10922  monoord2  10923  leexp1a  11031  bernneq  11098  apexp1  11156  nn0le2msqd  11157  faclbnd  11179  faclbnd3  11181  faclbnd6  11182  facubnd  11183  fihashdom  11243  zfz1isolemiso  11291  cjap  11672  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemlo  11779  resqrexlemcalc3  11782  absext  11829  xrnegiso  12028  xrminltinf  12038  fsumabs  12232  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  fprodle  12407  addmodlteqALT  12626  nn0seqcvgd  12819  algcvg  12826  algcvga  12829  eucalgcvga  12836  qnumgt0  12976  pcprendvds2  13070  pcpremul  13072  pcadd2  13120  2expltfac  13218  ctinfomlemom  13318  gzsumfzval  13711  mplsubgfilemcl  15090  ispsmet  15424  psmettri2  15429  ismet  15445  isxmet  15446  xmettri2  15462  blvalps  15489  blval  15490  comet  15600  bdxmet  15602  dvef  15828  cxplt  16018  rpcxple2  16020  rpcxplt2  16021  cxplt3  16022  apcxp2  16041  ltexp2  16043  logbleb  16063  logblt  16064  pellexlem3  16093  lgsdilem  16146  2lgslem1a2  16206  apdifflemr  17096  apdiff  17097