Theorem breq1i 4121

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 4117	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)

Syntax hints:   ↔ wb 105   = wceq 1398   class class class wbr 4114

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115

This theorem is referenced by:  eqbrtri  4135  brtpos0  6496  euen1  7055  euen1b  7056  2dom  7059  modom2  7075  infglbti  7329  pr2nelem  7501  pr2cv2  7506  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemaddq  8039  caucvgprprlem1  8040  gt0srpr  8079  caucvgsr  8133  mappsrprg  8135  map2psrprg  8136  pitonnlem1  8176  pitoregt0  8180  axprecex  8211  axpre-mulgt0  8218  axcaucvglemres  8230  lt0neg1  8759  le0neg1  8761  reclt1  9187  addltmul  9492  eluz2b1  9951  nn01to3  9967  xlt0neg1  10190  xle0neg1  10192  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  bernneq  11047  cbvsum  12070  expcnv  12215  cbvprod  12269  oddge22np1  12592  nn0o1gt2  12616  isprm3  12840  dvdsnprmd  12847  pw2dvdslemn  12887  ballotfilemi1  13189  txmetcnp  15509  sincosq1sgn  15817  sincosq3sgn  15819  sincosq4sgn  15820  logrpap0b  15867  gausslemma2dlem3  16062  konigsberglem5  16613