Theorem inss2 3302

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 3273	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3301	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3135	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3075   C_ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3082  df-ss 3089

This theorem is referenced by:  difin0  3441  bnd2  4105  ordin  4315  relin2  4666  relres  4855  ssrnres  4989  cnvcnv  4999  funinsn  5180  funimaexg  5215  fnresin2  5246  ssimaex  5490  ffvresb  5591  ofrfval  5998  ofvalg  5999  ofrval  6000  off  6002  ofres  6004  ofco  6008  offres  6041  tpostpos  6169  smores3  6198  tfrlem5  6219  tfrexlem  6239  erinxp  6511  pmresg  6578  unfiin  6822  ltrelpi  7156  peano5nnnn  7724  peano5nni  8747  rexanuz  10792  structcnvcnv  12014  restsspw  12169  eltg4i  12263  ntrss2  12329  ntrin  12332  isopn3  12333  resttopon  12379  restuni2  12385  cnrest2r  12445  cnptopresti  12446  cnptoprest  12447  lmss  12454  metrest  12714  tgioo  12754  peano5set  13309