Theorem breq1i 4032

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

Syntax hints:   ↔ wb 105   = wceq 1364   class class class wbr 4025

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2758  df-un 3152  df-sn 3620  df-pr 3621  df-op 3623  df-br 4026

This theorem is referenced by:  eqbrtri  4046  brtpos0  6285  euen1  6836  euen1b  6837  2dom  6839  infglbti  7063  pr2nelem  7230  caucvgprprlemnbj  7732  caucvgprprlemmu  7734  caucvgprprlemaddq  7747  caucvgprprlem1  7748  gt0srpr  7787  caucvgsr  7841  mappsrprg  7843  map2psrprg  7844  pitonnlem1  7884  pitoregt0  7888  axprecex  7919  axpre-mulgt0  7926  axcaucvglemres  7938  lt0neg1  8466  le0neg1  8468  reclt1  8894  addltmul  9196  eluz2b1  9643  nn01to3  9659  xlt0neg1  9880  xle0neg1  9882  iccshftr  10036  iccshftl  10038  iccdil  10040  icccntr  10042  bernneq  10687  cbvsum  11415  expcnv  11559  cbvprod  11613  oddge22np1  11933  nn0o1gt2  11957  isprm3  12167  dvdsnprmd  12174  pw2dvdslemn  12214  txmetcnp  14537  sincosq1sgn  14783  sincosq3sgn  14785  sincosq4sgn  14786  logrpap0b  14833