Theorem inss2 3425

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 3396	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3424	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3257	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3196   C_ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210

This theorem is referenced by:  difin0  3565  bnd2  4257  ordin  4476  relin2  4838  relres  5033  ssrnres  5171  cnvcnv  5181  funinsn  5370  funimaexg  5405  fnresin2  5439  ssimaex  5695  ffvresb  5798  ofrfval  6227  ofvalg  6228  ofrval  6229  off  6231  ofres  6233  ofco  6237  offres  6280  tpostpos  6410  smores3  6439  tfrlem5  6460  tfrexlem  6480  erinxp  6756  pmresg  6823  unfiin  7088  ltrelpi  7511  peano5nnnn  8079  peano5nni  9113  rexanuz  11499  bitsinv1  12473  structcnvcnv  13048  ressbasssd  13102  restsspw  13282  eltg4i  14729  ntrss2  14795  ntrin  14798  isopn3  14799  resttopon  14845  restuni2  14851  cnrest2r  14911  cnptopresti  14912  cnptoprest  14913  lmss  14920  metrest  15180  tgioo  15228  2sqlem8  15802  2sqlem9  15803  peano5set  16303