Theorem breq1i 4115

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

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

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 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109

This theorem is referenced by:  eqbrtri  4129  brtpos0  6482  euen1  7041  euen1b  7042  2dom  7045  modom2  7061  infglbti  7315  pr2nelem  7487  pr2cv2  7492  caucvgprprlemnbj  8007  caucvgprprlemmu  8009  caucvgprprlemaddq  8022  caucvgprprlem1  8023  gt0srpr  8062  caucvgsr  8116  mappsrprg  8118  map2psrprg  8119  pitonnlem1  8159  pitoregt0  8163  axprecex  8194  axpre-mulgt0  8201  axcaucvglemres  8213  lt0neg1  8741  le0neg1  8743  reclt1  9169  addltmul  9474  eluz2b1  9932  nn01to3  9948  xlt0neg1  10170  xle0neg1  10172  iccshftr  10326  iccshftl  10328  iccdil  10330  icccntr  10332  bernneq  11021  cbvsum  12041  expcnv  12186  cbvprod  12240  oddge22np1  12563  nn0o1gt2  12587  isprm3  12811  dvdsnprmd  12818  pw2dvdslemn  12858  txmetcnp  15375  sincosq1sgn  15683  sincosq3sgn  15685  sincosq4sgn  15686  logrpap0b  15733  gausslemma2dlem3  15928  konigsberglem5  16479