Theorem inss2 3394

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 3365	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3393	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3226	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3165   C_ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  difin0  3534  bnd2  4218  ordin  4433  relin2  4795  relres  4988  ssrnres  5126  cnvcnv  5136  funinsn  5324  funimaexg  5359  fnresin2  5393  ssimaex  5642  ffvresb  5745  ofrfval  6169  ofvalg  6170  ofrval  6171  off  6173  ofres  6175  ofco  6179  offres  6222  tpostpos  6352  smores3  6381  tfrlem5  6402  tfrexlem  6422  erinxp  6698  pmresg  6765  unfiin  7025  ltrelpi  7439  peano5nnnn  8007  peano5nni  9041  rexanuz  11332  bitsinv1  12306  structcnvcnv  12881  ressbasssd  12934  restsspw  13114  eltg4i  14560  ntrss2  14626  ntrin  14629  isopn3  14630  resttopon  14676  restuni2  14682  cnrest2r  14742  cnptopresti  14743  cnptoprest  14744  lmss  14751  metrest  15011  tgioo  15059  2sqlem8  15633  2sqlem9  15634  peano5set  15913