Theorem inss2 3430

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 3401	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3429	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3261	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3200   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  difin0  3570  bnd2  4269  ordin  4488  relin2  4852  relres  5047  ssrnres  5186  cnvcnv  5196  funinsn  5386  funimaexg  5421  fnresin2  5455  ssimaex  5716  ffvresb  5818  fnfvimad  5900  ofrfval  6253  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  ofco  6263  offres  6306  tpostpos  6473  smores3  6502  tfrlem5  6523  tfrexlem  6543  erinxp  6821  pmresg  6888  unfiin  7161  ltrelpi  7604  peano5nnnn  8172  peano5nni  9205  rexanuz  11628  bitsinv1  12603  structcnvcnv  13178  ressbasssd  13232  restsspw  13412  eltg4i  14866  ntrss2  14932  ntrin  14935  isopn3  14936  resttopon  14982  restuni2  14988  cnrest2r  15048  cnptopresti  15049  cnptoprest  15050  lmss  15057  metrest  15317  tgioo  15365  2sqlem8  15942  2sqlem9  15943  peano5set  16656