Theorem breq2i 4013

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

Hypothesis

Ref	Expression
breq1i.1	|- A = B

Assertion

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

Proof of Theorem breq2i

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

Syntax hints:   <-> wb 105   = wceq 1353   class class class wbr 4005

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  breqtri  4030  en1  6801  snnen2og  6861  1nen2  6863  pm54.43  7191  caucvgprprlemval  7689  caucvgprprlemmu  7696  caucvgsr  7803  pitonnlem1  7846  lt0neg2  8428  le0neg2  8430  negap0  8589  recexaplem2  8611  recgt1  8856  crap0  8917  addltmul  9157  nn0lt10b  9335  nn0lt2  9336  3halfnz  9352  xlt0neg2  9841  xle0neg2  9843  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fihashen1  10781  cjap0  10918  abs00ap  11073  xrmaxiflemval  11260  mertenslem2  11546  mertensabs  11547  3dvdsdec  11872  3dvds2dec  11873  ndvdsi  11940  3prm  12130  prmfac1  12154  prm23lt5  12265  sinhalfpilem  14297  sincosq1lem  14331  sincosq1sgn  14332  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  logrpap0b  14382  2lgsoddprmlem3  14544