Theorem inss2 3444

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

Syntax hints:   i^i cin 3212   C_ wss 3213

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3219  df-ss 3226

This theorem is referenced by:  difin0  3585  bnd2  4288  ordin  4508  relin2  4873  relres  5068  ssrnres  5207  cnvcnv  5217  funinsn  5407  funimaexg  5442  fnresin2  5476  ssimaex  5740  ffvresb  5842  fnfvimad  5924  ofrfval  6277  ofvalg  6278  ofrval  6279  off  6281  ofres  6283  ofco  6287  offres  6330  tpostpos  6497  smores3  6526  tfrlem5  6547  tfrexlem  6567  erinxp  6845  pmresg  6912  unfiin  7188  ltrelpi  7641  peano5nnnn  8209  peano5nni  9242  rexanuz  11677  bitsinv1  12652  structcnvcnv  13245  ressbasssd  13299  restsspw  13479  eltg4i  14937  ntrss2  15003  ntrin  15006  isopn3  15007  resttopon  15053  restuni2  15059  cnrest2r  15119  cnptopresti  15120  cnptoprest  15121  lmss  15128  metrest  15388  tgioo  15436  2sqlem8  16013  2sqlem9  16014  peano5set  16727