Theorem ineq2i 3198

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1	|- A = B

Assertion

Ref	Expression
ineq2i	|- ( C i^i A ) = ( C i^i B )

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 |- A = B
2		ineq2 3195	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	ax-mp 7	1 |- ( C i^i A ) = ( C i^i B )

Syntax hints:   = wceq 1289   i^i cin 2998

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-in 3005

This theorem is referenced by:  in4  3216  inindir  3218  indif2  3243  difun1  3259  dfrab3ss  3277  dfif3  3406  intunsn  3726  rint0  3727  riin0  3801  res0  4717  resres  4725  resundi  4726  resindi  4728  inres  4730  resiun2  4733  resopab  4756  dfse2  4805  dminxp  4875  imainrect  4876  resdmres  4922  funimacnv  5090  unfiin  6636  sbthlemi5  6670  dmaddpi  6884  dmmulpi  6885  fsumiun  10871