Theorem breq1i 4010

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

Syntax hints:   ↔ wb 105   = wceq 1353   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  eqbrtri  4024  brtpos0  6252  euen1  6801  euen1b  6802  2dom  6804  infglbti  7023  pr2nelem  7189  caucvgprprlemnbj  7691  caucvgprprlemmu  7693  caucvgprprlemaddq  7706  caucvgprprlem1  7707  gt0srpr  7746  caucvgsr  7800  mappsrprg  7802  map2psrprg  7803  pitonnlem1  7843  pitoregt0  7847  axprecex  7878  axpre-mulgt0  7885  axcaucvglemres  7897  lt0neg1  8424  le0neg1  8426  reclt1  8852  addltmul  9154  eluz2b1  9600  nn01to3  9616  xlt0neg1  9837  xle0neg1  9839  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  bernneq  10640  cbvsum  11367  expcnv  11511  cbvprod  11565  oddge22np1  11885  nn0o1gt2  11909  isprm3  12117  dvdsnprmd  12124  pw2dvdslemn  12164  txmetcnp  13988  sincosq1sgn  14217  sincosq3sgn  14219  sincosq4sgn  14220  logrpap0b  14267