Theorem breq1i 3900

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

Syntax hints:   ↔ wb 104   = wceq 1312   class class class wbr 3893

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-br 3894

This theorem is referenced by:  eqbrtri  3912  brtpos0  6101  euen1  6648  euen1b  6649  2dom  6651  infglbti  6862  pr2nelem  6994  caucvgprprlemnbj  7443  caucvgprprlemmu  7445  caucvgprprlemaddq  7458  caucvgprprlem1  7459  gt0srpr  7485  caucvgsr  7538  pitonnlem1  7574  pitoregt0  7578  axprecex  7609  axpre-mulgt0  7616  axcaucvglemres  7628  lt0neg1  8143  le0neg1  8145  reclt1  8558  addltmul  8854  eluz2b1  9291  nn01to3  9305  xlt0neg1  9508  xle0neg1  9510  iccshftr  9664  iccshftl  9666  iccdil  9668  icccntr  9670  bernneq  10299  cbvsum  11015  expcnv  11159  oddge22np1  11420  nn0o1gt2  11444  isprm3  11639  dvdsnprmd  11646  pw2dvdslemn  11682  txmetcnp  12501