Theorem inss2 3224

Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)

Assertion

Ref	Expression
inss2	|- ( A i^i B ) C_ B

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 3195	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3223	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstr3i 3060	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3001   C_ wss 3002

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 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2624  df-in 3008  df-ss 3015

This theorem is referenced by:  difin0  3362  bnd2  4016  ordin  4223  relin2  4571  relres  4756  ssrnres  4888  cnvcnv  4898  funinsn  5078  funimaexg  5113  fnresin2  5144  ssimaex  5380  ffvresb  5477  ofrfval  5880  fnofval  5881  ofrval  5882  off  5884  ofres  5885  ofco  5889  offres  5922  tpostpos  6045  smores3  6074  tfrlem5  6095  tfrexlem  6115  erinxp  6382  pmresg  6449  unfiin  6692  ltrelpi  6946  peano5nnnn  7490  peano5nni  8488  rexanuz  10484  structcnvcnv  11573  restsspw  11725  eltg4i  11818  ntrss2  11884  ntrin  11887  isopn3  11888  peano5set  12139