Theorem breq12d 4018

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   class class class wbr 4005

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  breq123d  4019  3brtr3d  4036  3brtr4d  4037  pocl  4305  csbcnvg  4813  cnvpom  5173  sbcfung  5242  isoeq1  5804  isocnv  5814  isotr  5819  caovordig  6042  caovordg  6044  caovord2d  6046  caovord  6048  ofrfval  6093  ofrval  6095  ofrfval2  6101  caofref  6106  fundmeng  6809  xpsneng  6824  xpcomeng  6830  xpdom2g  6834  phplem3g  6858  php5  6860  php5dom  6865  exmidapne  7261  nqtri3or  7397  ltsonq  7399  ltanqg  7401  ltmnqg  7402  lt2addnq  7405  lt2mulnq  7406  prarloclemarch  7419  ltrnqg  7421  ltnnnq  7424  prarloclemlt  7494  addlocprlemgt  7535  mullocprlem  7571  addextpr  7622  recexprlemss1l  7636  recexprlemss1u  7637  recexpr  7639  caucvgprlemcanl  7645  cauappcvgprlemm  7646  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlemlim  7662  cauappcvgpr  7663  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexb  7708  caucvgprprlem1  7710  lttrsr  7763  ltposr  7764  ltsosr  7765  ltasrg  7771  aptisr  7780  mulextsr1lem  7781  mulextsr1  7782  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  caucvgsr  7803  axpre-ltirr  7883  axpre-ltadd  7887  axpre-mulgt0  7888  axpre-mulext  7889  axcaucvglemcau  7899  axcaucvglemres  7900  ltadd2  8378  ltadd1  8388  leadd2  8390  reapval  8535  reapmul1  8554  remulext2  8559  apreim  8562  apirr  8564  apsym  8565  apcotr  8566  apadd1  8567  apadd2  8568  apneg  8570  mulext1  8571  mulext2  8572  apti  8581  apsub1  8601  subap0  8602  apmul1  8747  apmul2  8748  apdivmuld  8772  ltmul2  8815  lemul2  8816  ltdiv1  8827  ltdiv2  8846  ledivdiv  8849  lediv2  8850  negiso  8914  div4p1lem1div2  9174  qapne  9641  nn0ledivnn  9769  xleadd1  9877  xltadd1  9878  xltadd2  9879  xsubge0  9883  xleaddadd  9889  qtri3or  10245  frecfzennn  10428  monoord  10478  monoord2  10479  leexp1a  10577  bernneq  10643  apexp1  10700  nn0le2msqd  10701  faclbnd  10723  faclbnd3  10725  faclbnd6  10726  facubnd  10727  fihashdom  10785  zfz1isolemiso  10821  cjap  10917  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemlo  11024  resqrexlemcalc3  11027  absext  11074  xrnegiso  11272  xrminltinf  11282  fsumabs  11475  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  fprodle  11650  addmodlteqALT  11867  nn0seqcvgd  12043  algcvg  12050  algcvga  12053  eucalgcvga  12060  qnumgt0  12200  pcprendvds2  12293  pcpremul  12295  ctinfomlemom  12430  ispsmet  13862  psmettri2  13867  ismet  13883  isxmet  13884  xmettri2  13900  blvalps  13927  blval  13928  comet  14038  bdxmet  14040  dvef  14227  cxplt  14375  rpcxple2  14377  rpcxplt2  14378  cxplt3  14379  apcxp2  14397  ltexp2  14399  logbleb  14418  logblt  14419  lgsdilem  14467  apdifflemr  14834  apdiff  14835