Theorem breq1i 4095

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
breq1i	⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		breq1 4091	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 105   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  eqbrtri  4109  brtpos0  6418  euen1  6976  euen1b  6977  2dom  6980  modom2  6995  infglbti  7224  pr2nelem  7396  pr2cv2  7401  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemaddq  7928  caucvgprprlem1  7929  gt0srpr  7968  caucvgsr  8022  mappsrprg  8024  map2psrprg  8025  pitonnlem1  8065  pitoregt0  8069  axprecex  8100  axpre-mulgt0  8107  axcaucvglemres  8119  lt0neg1  8648  le0neg1  8650  reclt1  9076  addltmul  9381  eluz2b1  9835  nn01to3  9851  xlt0neg1  10073  xle0neg1  10075  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  bernneq  10923  cbvsum  11938  expcnv  12083  cbvprod  12137  oddge22np1  12460  nn0o1gt2  12484  isprm3  12708  dvdsnprmd  12715  pw2dvdslemn  12755  txmetcnp  15261  sincosq1sgn  15569  sincosq3sgn  15571  sincosq4sgn  15572  logrpap0b  15619  gausslemma2dlem3  15811  konigsberglem5  16362