Theorem breq2i 3901

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 3897	. 2 |- ( A = B -> ( C R A <-> C R B ) )
3	1, 2	ax-mp 7	1 |- ( C R A <-> C R B )

Syntax hints:   <-> wb 104   = wceq 1312   class class class wbr 3893

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-br 3894

This theorem is referenced by:  breqtri  3916  en1  6645  snnen2og  6704  1nen2  6706  pm54.43  6993  caucvgprprlemval  7438  caucvgprprlemmu  7445  caucvgsr  7538  pitonnlem1  7574  lt0neg2  8144  le0neg2  8146  negap0  8304  recexaplem2  8320  recgt1  8559  crap0  8620  addltmul  8854  nn0lt10b  9029  nn0lt2  9030  3halfnz  9046  xlt0neg2  9509  xle0neg2  9511  iccshftr  9664  iccshftl  9666  iccdil  9668  icccntr  9670  fihashen1  10432  cjap0  10566  abs00ap  10720  xrmaxiflemval  10905  mertenslem2  11191  mertensabs  11192  3dvdsdec  11404  3dvds2dec  11405  ndvdsi  11472  3prm  11649  prmfac1  11670