Theorem breq1i 4051

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

Syntax hints:   ↔ wb 105   = wceq 1373   class class class wbr 4044

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  eqbrtri  4065  brtpos0  6338  euen1  6894  euen1b  6895  2dom  6897  infglbti  7127  pr2nelem  7299  caucvgprprlemnbj  7806  caucvgprprlemmu  7808  caucvgprprlemaddq  7821  caucvgprprlem1  7822  gt0srpr  7861  caucvgsr  7915  mappsrprg  7917  map2psrprg  7918  pitonnlem1  7958  pitoregt0  7962  axprecex  7993  axpre-mulgt0  8000  axcaucvglemres  8012  lt0neg1  8541  le0neg1  8543  reclt1  8969  addltmul  9274  eluz2b1  9722  nn01to3  9738  xlt0neg1  9960  xle0neg1  9962  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  bernneq  10805  cbvsum  11671  expcnv  11815  cbvprod  11869  oddge22np1  12192  nn0o1gt2  12216  isprm3  12440  dvdsnprmd  12447  pw2dvdslemn  12487  txmetcnp  14990  sincosq1sgn  15298  sincosq3sgn  15300  sincosq4sgn  15301  logrpap0b  15348  gausslemma2dlem3  15540