Theorem ineq2i 3335

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 3332	. 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 1353   i^i cin 3130

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-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-in 3137

This theorem is referenced by:  in4  3353  inindir  3355  indif2  3381  difun1  3397  dfrab3ss  3415  dfif3  3549  intunsn  3884  rint0  3885  riin0  3960  res0  4913  resres  4921  resundi  4922  resindi  4924  inres  4926  resiun2  4929  resopab  4953  dfse2  5003  dminxp  5075  imainrect  5076  resdmres  5122  funimacnv  5294  unfiin  6928  sbthlemi5  6963  dmaddpi  7327  dmmulpi  7328  fsumiun  11488  ressval2  12529  ressval3d  12534