Theorem breq12d 4016

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

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

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  breq123d  4017  3brtr3d  4034  3brtr4d  4035  pocl  4303  csbcnvg  4811  cnvpom  5171  sbcfung  5240  isoeq1  5801  isocnv  5811  isotr  5816  caovordig  6039  caovordg  6041  caovord2d  6043  caovord  6045  ofrfval  6090  ofrval  6092  ofrfval2  6098  caofref  6103  fundmeng  6806  xpsneng  6821  xpcomeng  6827  xpdom2g  6831  phplem3g  6855  php5  6857  php5dom  6862  exmidapne  7258  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  lt2addnq  7402  lt2mulnq  7403  prarloclemarch  7416  ltrnqg  7418  ltnnnq  7421  prarloclemlt  7491  addlocprlemgt  7532  mullocprlem  7568  addextpr  7619  recexprlemss1l  7633  recexprlemss1u  7634  recexpr  7636  caucvgprlemcanl  7642  cauappcvgprlemm  7643  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlemlim  7659  cauappcvgpr  7660  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexb  7705  caucvgprprlem1  7707  lttrsr  7760  ltposr  7761  ltsosr  7762  ltasrg  7768  aptisr  7777  mulextsr1lem  7778  mulextsr1  7779  caucvgsrlemcau  7791  caucvgsrlemgt1  7793  caucvgsrlemoffcau  7796  caucvgsrlemoffres  7798  caucvgsr  7800  axpre-ltirr  7880  axpre-ltadd  7884  axpre-mulgt0  7885  axpre-mulext  7886  axcaucvglemcau  7896  axcaucvglemres  7897  ltadd2  8375  ltadd1  8385  leadd2  8387  reapval  8532  reapmul1  8551  remulext2  8556  apreim  8559  apirr  8561  apsym  8562  apcotr  8563  apadd1  8564  apadd2  8565  apneg  8567  mulext1  8568  mulext2  8569  apti  8578  apsub1  8598  subap0  8599  apmul1  8744  apmul2  8745  apdivmuld  8769  ltmul2  8812  lemul2  8813  ltdiv1  8824  ltdiv2  8843  ledivdiv  8846  lediv2  8847  negiso  8911  div4p1lem1div2  9171  qapne  9638  nn0ledivnn  9766  xleadd1  9874  xltadd1  9875  xltadd2  9876  xsubge0  9880  xleaddadd  9886  qtri3or  10242  frecfzennn  10425  monoord  10475  monoord2  10476  leexp1a  10574  bernneq  10640  apexp1  10697  nn0le2msqd  10698  faclbnd  10720  faclbnd3  10722  faclbnd6  10723  facubnd  10724  fihashdom  10782  zfz1isolemiso  10818  cjap  10914  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemlo  11021  resqrexlemcalc3  11024  absext  11071  xrnegiso  11269  xrminltinf  11279  fsumabs  11472  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  fprodle  11647  addmodlteqALT  11864  nn0seqcvgd  12040  algcvg  12047  algcvga  12050  eucalgcvga  12057  qnumgt0  12197  pcprendvds2  12290  pcpremul  12292  ctinfomlemom  12427  ispsmet  13793  psmettri2  13798  ismet  13814  isxmet  13815  xmettri2  13831  blvalps  13858  blval  13859  comet  13969  bdxmet  13971  dvef  14158  cxplt  14306  rpcxple2  14308  rpcxplt2  14309  cxplt3  14310  apcxp2  14328  ltexp2  14330  logbleb  14349  logblt  14350  lgsdilem  14398  apdifflemr  14765  apdiff  14766