Theorem breq2i 4117

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 4113	. 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 1398   class class class wbr 4109

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  breqtri  4134  en1  7039  snnen2og  7113  1nen2  7115  pm54.43  7487  caucvgprprlemval  8003  caucvgprprlemmu  8010  caucvgsr  8117  pitonnlem1  8160  lt0neg2  8743  le0neg2  8745  negap0  8904  recexaplem2  8926  recgt1  9171  crap0  9232  addltmul  9475  nn0lt10b  9658  nn0lt2  9659  3halfnz  9675  xlt0neg2  10172  xle0neg2  10174  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fihashen1  11162  swrdccatin2  11421  pfxccat3  11426  cjap0  11592  abs00ap  11747  xrmaxiflemval  11935  mertenslem2  12222  mertensabs  12223  3dvdsdec  12551  3dvds2dec  12552  ndvdsi  12619  bitsfzo  12641  3prm  12825  prmfac1  12849  prm23lt5  12961  dec2dvds  13109  dec5dvds2  13111  sinhalfpilem  15656  sincosq1lem  15690  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  logrpap0b  15741  gausslemma2dlem1a  15931  2lgsoddprmlem3  15984  konigsberglem4  16486