Theorem breq1i 4066

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  eqbrtri  4080  brtpos0  6361  euen1  6917  euen1b  6918  2dom  6921  infglbti  7153  pr2nelem  7325  pr2cv2  7330  caucvgprprlemnbj  7841  caucvgprprlemmu  7843  caucvgprprlemaddq  7856  caucvgprprlem1  7857  gt0srpr  7896  caucvgsr  7950  mappsrprg  7952  map2psrprg  7953  pitonnlem1  7993  pitoregt0  7997  axprecex  8028  axpre-mulgt0  8035  axcaucvglemres  8047  lt0neg1  8576  le0neg1  8578  reclt1  9004  addltmul  9309  eluz2b1  9757  nn01to3  9773  xlt0neg1  9995  xle0neg1  9997  iccshftr  10151  iccshftl  10153  iccdil  10155  icccntr  10157  bernneq  10842  cbvsum  11786  expcnv  11930  cbvprod  11984  oddge22np1  12307  nn0o1gt2  12331  isprm3  12555  dvdsnprmd  12562  pw2dvdslemn  12602  txmetcnp  15105  sincosq1sgn  15413  sincosq3sgn  15415  sincosq4sgn  15416  logrpap0b  15463  gausslemma2dlem3  15655