Theorem breq12i 5084

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

Syntax hints:   ↔ wb 208   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  3brtr3g  5108  3brtr4g  5109  caovord2  7572  domunfican  9226  ltsonq  10887  ltanq  10889  ltmnq  10890  prlem934  10951  prlem936  10965  ltsosr  11012  ltasr  11018  ltneg  11645  leneg  11648  lt2sqi  14146  le2sqi  14147  nn0le2msqi  14224  2sqreuop  27447  2sqreuopnn  27448  2sqreuoplt  27449  2sqreuopltb  27450  2sqreuopnnlt  27451  2sqreuopnnltb  27452  axlowdimlem6  29038  upgrwlkcompim  29733  clwlkcompbp  29872  mdsldmd1i  32424  fldext2chn  33924  constrextdg2lem  33944  divcnvlin  35976  ditgeq123i  36452  cbvditgvw2  36492  relowlpssretop  37741  2ap1caineq  42645  fsumlessf  46036  climlimsupcex  46226  liminfltlimsupex  46238  liminflelimsupcex  46254  sge0xaddlem2  46891  eubrdm  47513  isgrlim2  48488  iscmgmALT  48729  iscsgrpALT  48731