Theorem ineq2i 3358

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 3355	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	ax-mp 5	1 |- ( C i^i A ) = ( C i^i B )

Syntax hints:   = wceq 1364   i^i cin 3153

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160

This theorem is referenced by:  in4  3376  inindir  3378  indif2  3404  difun1  3420  dfrab3ss  3438  dfif3  3571  intunsn  3909  rint0  3910  riin0  3985  res0  4947  resres  4955  resundi  4956  resindi  4958  inres  4960  resiun2  4963  resopab  4987  dfse2  5039  dminxp  5111  imainrect  5112  resdmres  5158  funimacnv  5331  unfiin  6984  sbthlemi5  7022  dmaddpi  7387  dmmulpi  7388  fsumiun  11623  ressval2  12687  ressval3d  12693  lgsquadlem3  15236