Theorem breq12i 5112

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵
breq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
breq12i	⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

Proof of Theorem breq12i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		breq12 5108	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  3brtr3g  5138  3brtr4g  5139  caovord2  7622  domunfican  9291  ltsonq  11011  ltanq  11013  ltmnq  11014  prlem934  11075  prlem936  11089  ltsosr  11136  ltasr  11142  ltneg  11771  leneg  11774  lt2sqi  14286  le2sqi  14287  nn0le2msqi  14364  2sqreuop  27738  2sqreuopnn  27739  2sqreuoplt  27740  2sqreuopltb  27741  2sqreuopnnlt  27742  2sqreuopnnltb  27743  axlowdimlem6  29444  upgrwlkcompim  30142  clwlkcompbp  30288  mdsldmd1i  32852  fldext2chn  34279  constrextdg2lem  34299  divcnvlin  36413  ditgeq123i  36914  cbvditgvw2  36954  relowlpssretop  38201  2ap1caineq  43109  fsumlessf  46505  climlimsupcex  46695  liminfltlimsupex  46707  liminflelimsupcex  46723  sge0xaddlem2  47360  eubrdm  48022  isgrlim2  48997  iscmgmALT  49237  iscsgrpALT  49239