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  6417  euen1  6975  euen1b  6976  2dom  6979  modom2  6994  infglbti  7223  pr2nelem  7395  pr2cv2  7400  caucvgprprlemnbj  7912  caucvgprprlemmu  7914  caucvgprprlemaddq  7927  caucvgprprlem1  7928  gt0srpr  7967  caucvgsr  8021  mappsrprg  8023  map2psrprg  8024  pitonnlem1  8064  pitoregt0  8068  axprecex  8099  axpre-mulgt0  8106  axcaucvglemres  8118  lt0neg1  8647  le0neg1  8649  reclt1  9075  addltmul  9380  eluz2b1  9834  nn01to3  9850  xlt0neg1  10072  xle0neg1  10074  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  bernneq  10921  cbvsum  11920  expcnv  12064  cbvprod  12118  oddge22np1  12441  nn0o1gt2  12465  isprm3  12689  dvdsnprmd  12696  pw2dvdslemn  12736  txmetcnp  15241  sincosq1sgn  15549  sincosq3sgn  15551  sincosq4sgn  15552  logrpap0b  15599  gausslemma2dlem3  15791