Theorem breq1i 4116

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  eqbrtri  4130  brtpos0  6483  euen1  7042  euen1b  7043  2dom  7046  modom2  7062  infglbti  7316  pr2nelem  7488  pr2cv2  7493  caucvgprprlemnbj  8008  caucvgprprlemmu  8010  caucvgprprlemaddq  8023  caucvgprprlem1  8024  gt0srpr  8063  caucvgsr  8117  mappsrprg  8119  map2psrprg  8120  pitonnlem1  8160  pitoregt0  8164  axprecex  8195  axpre-mulgt0  8202  axcaucvglemres  8214  lt0neg1  8742  le0neg1  8744  reclt1  9170  addltmul  9475  eluz2b1  9933  nn01to3  9949  xlt0neg1  10171  xle0neg1  10173  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  bernneq  11022  cbvsum  12045  expcnv  12190  cbvprod  12244  oddge22np1  12567  nn0o1gt2  12591  isprm3  12815  dvdsnprmd  12822  pw2dvdslemn  12862  txmetcnp  15383  sincosq1sgn  15691  sincosq3sgn  15693  sincosq4sgn  15694  logrpap0b  15741  gausslemma2dlem3  15936  konigsberglem5  16487