Theorem breq1i 4052

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 4048	. 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 1373   class class class wbr 4045

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 4046

This theorem is referenced by:  eqbrtri  4066  brtpos0  6340  euen1  6896  euen1b  6897  2dom  6899  infglbti  7129  pr2nelem  7301  caucvgprprlemnbj  7808  caucvgprprlemmu  7810  caucvgprprlemaddq  7823  caucvgprprlem1  7824  gt0srpr  7863  caucvgsr  7917  mappsrprg  7919  map2psrprg  7920  pitonnlem1  7960  pitoregt0  7964  axprecex  7995  axpre-mulgt0  8002  axcaucvglemres  8014  lt0neg1  8543  le0neg1  8545  reclt1  8971  addltmul  9276  eluz2b1  9724  nn01to3  9740  xlt0neg1  9962  xle0neg1  9964  iccshftr  10118  iccshftl  10120  iccdil  10122  icccntr  10124  bernneq  10807  cbvsum  11704  expcnv  11848  cbvprod  11902  oddge22np1  12225  nn0o1gt2  12249  isprm3  12473  dvdsnprmd  12480  pw2dvdslemn  12520  txmetcnp  15023  sincosq1sgn  15331  sincosq3sgn  15333  sincosq4sgn  15334  logrpap0b  15381  gausslemma2dlem3  15573