Theorem breq1i 4008

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 4004	. 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 1353   class class class wbr 4001

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002

This theorem is referenced by:  eqbrtri  4022  brtpos0  6248  euen1  6797  euen1b  6798  2dom  6800  infglbti  7019  pr2nelem  7185  caucvgprprlemnbj  7687  caucvgprprlemmu  7689  caucvgprprlemaddq  7702  caucvgprprlem1  7703  gt0srpr  7742  caucvgsr  7796  mappsrprg  7798  map2psrprg  7799  pitonnlem1  7839  pitoregt0  7843  axprecex  7874  axpre-mulgt0  7881  axcaucvglemres  7893  lt0neg1  8419  le0neg1  8421  reclt1  8847  addltmul  9149  eluz2b1  9595  nn01to3  9611  xlt0neg1  9832  xle0neg1  9834  iccshftr  9988  iccshftl  9990  iccdil  9992  icccntr  9994  bernneq  10633  cbvsum  11359  expcnv  11503  cbvprod  11557  oddge22np1  11876  nn0o1gt2  11900  isprm3  12108  dvdsnprmd  12115  pw2dvdslemn  12155  txmetcnp  13800  sincosq1sgn  14029  sincosq3sgn  14031  sincosq4sgn  14032  logrpap0b  14079