Theorem breq1i 4040

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypothesis

Ref	Expression
breq1i.1	|- A = B

Assertion

Ref	Expression
breq1i	|- ( A R C <-> B R C )

Proof of Theorem breq1i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq1 4036	. 2 |- ( A = B -> ( A R C <-> B R C ) )
3	1, 2	ax-mp 5	1 |- ( A R C <-> B R C )

Syntax hints:   <-> wb 105   = wceq 1364   class class class wbr 4033

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034

This theorem is referenced by:  eqbrtri  4054  brtpos0  6310  euen1  6861  euen1b  6862  2dom  6864  infglbti  7091  pr2nelem  7258  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemaddq  7775  caucvgprprlem1  7776  gt0srpr  7815  caucvgsr  7869  mappsrprg  7871  map2psrprg  7872  pitonnlem1  7912  pitoregt0  7916  axprecex  7947  axpre-mulgt0  7954  axcaucvglemres  7966  lt0neg1  8495  le0neg1  8497  reclt1  8923  addltmul  9228  eluz2b1  9675  nn01to3  9691  xlt0neg1  9913  xle0neg1  9915  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  bernneq  10752  cbvsum  11525  expcnv  11669  cbvprod  11723  oddge22np1  12046  nn0o1gt2  12070  isprm3  12286  dvdsnprmd  12293  pw2dvdslemn  12333  txmetcnp  14754  sincosq1sgn  15062  sincosq3sgn  15064  sincosq4sgn  15065  logrpap0b  15112  gausslemma2dlem3  15304