Theorem inss2 3348

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 3319	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3347	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3180	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3120   C_ wss 3121

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  difin0  3488  bnd2  4159  ordin  4370  relin2  4730  relres  4919  ssrnres  5053  cnvcnv  5063  funinsn  5247  funimaexg  5282  fnresin2  5313  ssimaex  5557  ffvresb  5659  ofrfval  6069  ofvalg  6070  ofrval  6071  off  6073  ofres  6075  ofco  6079  offres  6114  tpostpos  6243  smores3  6272  tfrlem5  6293  tfrexlem  6313  erinxp  6587  pmresg  6654  unfiin  6903  ltrelpi  7286  peano5nnnn  7854  peano5nni  8881  rexanuz  10952  structcnvcnv  12432  restsspw  12589  eltg4i  12849  ntrss2  12915  ntrin  12918  isopn3  12919  resttopon  12965  restuni2  12971  cnrest2r  13031  cnptopresti  13032  cnptoprest  13033  lmss  13040  metrest  13300  tgioo  13340  2sqlem8  13753  2sqlem9  13754  peano5set  13975