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  7612  exmidapne  7627  nqtri3or  7764  ltsonq  7766  ltanqg  7768  ltmnqg  7769  lt2addnq  7772  lt2mulnq  7773  prarloclemarch  7786  ltrnqg  7788  ltnnnq  7791  prarloclemlt  7861  addlocprlemgt  7902  mullocprlem  7938  addextpr  7989  recexprlemss1l  8003  recexprlemss1u  8004  recexpr  8006  caucvgprlemcanl  8012  cauappcvgprlemm  8013  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexb  8075  caucvgprprlem1  8077  lttrsr  8130  ltposr  8131  ltsosr  8132  ltasrg  8138  aptisr  8147  mulextsr1lem  8148  mulextsr1  8149  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsr  8170  axpre-ltirr  8250  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  axcaucvglemcau  8266  axcaucvglemres  8267  ltadd2  8749  ltadd1  8759  leadd2  8761  reapval  8907  reapmul1  8926  remulext2  8931  apreim  8934  apirr  8936  apsym  8937  apcotr  8938  apadd1  8939  apadd2  8940  apneg  8942  mulext1  8943  mulext2  8944  apti  8953  apsub1  8973  subap0  8974  apmul1  9121  apmul2  9122  apdivmuld  9146  ltmul2  9189  lemul2  9190  ltdiv1  9201  ltdiv2  9220  ledivdiv  9223  lediv2  9224  negiso  9288  div4p1lem1div2  9564  qapne  10049  nn0ledivnn  10179  xleadd1  10288  xltadd1  10289  xltadd2  10290  xsubge0  10294  xleaddadd  10300  qtri3or  10686  frecfzennn  10878  monoord  10937  monoord2  10938  leexp1a  11046  bernneq  11113  apexp1  11172  nn0le2msqd  11173  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  facubnd  11199  fihashdom  11259  zfz1isolemiso  11307  cjap  11688  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemlo  11795  resqrexlemcalc3  11798  absext  11845  xrnegiso  12047  xrminltinf  12057  fsumabs  12251  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  fprodle  12426  addmodlteqALT  12645  nn0seqcvgd  12838  algcvg  12845  algcvga  12848  eucalgcvga  12855  qnumgt0  12997  pcprendvds2  13093  pcpremul  13095  pcadd2  13143  2expltfac  13242  ctinfomlemom  13370  gzsumfzval  13764  mplsubgfilemcl  15181  ispsmet  15515  psmettri2  15520  ismet  15536  isxmet  15537  xmettri2  15553  blvalps  15580  blval  15581  comet  15691  bdxmet  15693  dvef  15919  cxplt  16113  rpcxple2  16115  rpcxplt2  16116  cxplt3  16117  apcxp2  16136  ltexp2  16138  logbleb  16158  logblt  16159  pellexlem3  16192  ppiqltx  16242  chtqub  16257  bclbnd  16268  prmefexple  16269  bposlem5  16276  bposlem6  16277  bposlem7  16278  lgsdilem  16312  2lgslem1a2  16372  apdifflemr  17263  apdiff  17264