Theorem breq12i 5116

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 5112	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  3brtr3g  5142  3brtr4g  5143  caovord2  7629  domunfican  9294  ltsonq  10981  ltanq  10983  ltmnq  10984  prlem934  11045  prlem936  11059  ltsosr  11106  ltasr  11112  ltneg  11741  leneg  11744  lt2sqi  14255  le2sqi  14256  nn0le2msqi  14333  2sqreuop  27696  2sqreuopnn  27697  2sqreuoplt  27698  2sqreuopltb  27699  2sqreuopnnlt  27700  2sqreuopnnltb  27701  axlowdimlem6  29390  upgrwlkcompim  30088  clwlkcompbp  30234  mdsldmd1i  32798  fldext2chn  34225  constrextdg2lem  34245  divcnvlin  36299  ditgeq123i  36816  cbvditgvw2  36856  relowlpssretop  38105  2ap1caineq  42998  fsumlessf  46394  climlimsupcex  46584  liminfltlimsupex  46596  liminflelimsupcex  46612  sge0xaddlem2  47249  eubrdm  47911  isgrlim2  48886  iscmgmALT  49126  iscsgrpALT  49128