Theorem breq12d 4096

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq123d  4097  3brtr3d  4114  3brtr4d  4115  pocl  4394  csbcnvg  4906  cnvpom  5271  sbcfung  5342  isoeq1  5931  isocnv  5941  isotr  5946  caovordig  6177  caovordg  6179  caovord2d  6181  caovord  6183  ofrfval  6233  ofrval  6235  ofrfval2  6241  caofref  6249  fundmeng  6968  xpsneng  6989  xpcomeng  6995  xpdom2g  6999  phplem3g  7025  php5  7027  php5dom  7032  exmidpw2en  7085  exmidapne  7457  nqtri3or  7594  ltsonq  7596  ltanqg  7598  ltmnqg  7599  lt2addnq  7602  lt2mulnq  7603  prarloclemarch  7616  ltrnqg  7618  ltnnnq  7621  prarloclemlt  7691  addlocprlemgt  7732  mullocprlem  7768  addextpr  7819  recexprlemss1l  7833  recexprlemss1u  7834  recexpr  7836  caucvgprlemcanl  7842  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgpr  7880  caucvgprprlemell  7883  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexb  7905  caucvgprprlem1  7907  lttrsr  7960  ltposr  7961  ltsosr  7962  ltasrg  7968  aptisr  7977  mulextsr1lem  7978  mulextsr1  7979  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  axpre-ltirr  8080  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  axcaucvglemcau  8096  axcaucvglemres  8097  ltadd2  8577  ltadd1  8587  leadd2  8589  reapval  8734  reapmul1  8753  remulext2  8758  apreim  8761  apirr  8763  apsym  8764  apcotr  8765  apadd1  8766  apadd2  8767  apneg  8769  mulext1  8770  mulext2  8771  apti  8780  apsub1  8800  subap0  8801  apmul1  8946  apmul2  8947  apdivmuld  8971  ltmul2  9014  lemul2  9015  ltdiv1  9026  ltdiv2  9045  ledivdiv  9048  lediv2  9049  negiso  9113  div4p1lem1div2  9376  qapne  9846  nn0ledivnn  9975  xleadd1  10083  xltadd1  10084  xltadd2  10085  xsubge0  10089  xleaddadd  10095  qtri3or  10472  frecfzennn  10660  monoord  10719  monoord2  10720  leexp1a  10828  bernneq  10894  apexp1  10952  nn0le2msqd  10953  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  facubnd  10979  fihashdom  11037  zfz1isolemiso  11074  cjap  11432  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemlo  11539  resqrexlemcalc3  11542  absext  11589  xrnegiso  11788  xrminltinf  11798  fsumabs  11991  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  fprodle  12166  addmodlteqALT  12385  nn0seqcvgd  12578  algcvg  12585  algcvga  12588  eucalgcvga  12595  qnumgt0  12735  pcprendvds2  12829  pcpremul  12831  pcadd2  12879  2expltfac  12977  ctinfomlemom  13013  gsumfzval  13439  mplsubgfilemcl  14678  ispsmet  15012  psmettri2  15017  ismet  15033  isxmet  15034  xmettri2  15050  blvalps  15077  blval  15078  comet  15188  bdxmet  15190  dvef  15416  cxplt  15605  rpcxple2  15607  rpcxplt2  15608  cxplt3  15609  apcxp2  15628  ltexp2  15630  logbleb  15650  logblt  15651  lgsdilem  15721  2lgslem1a2  15781  apdifflemr  16475  apdiff  16476