Theorem inss2 3357

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 3328	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3356	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3189	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3129   C_ wss 3130

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-in 3136  df-ss 3143

This theorem is referenced by:  difin0  3497  bnd2  4174  ordin  4386  relin2  4746  relres  4936  ssrnres  5072  cnvcnv  5082  funinsn  5266  funimaexg  5301  fnresin2  5332  ssimaex  5578  ffvresb  5680  ofrfval  6091  ofvalg  6092  ofrval  6093  off  6095  ofres  6097  ofco  6101  offres  6136  tpostpos  6265  smores3  6294  tfrlem5  6315  tfrexlem  6335  erinxp  6609  pmresg  6676  unfiin  6925  ltrelpi  7323  peano5nnnn  7891  peano5nni  8922  rexanuz  10997  structcnvcnv  12478  ressbasssd  12529  restsspw  12698  eltg4i  13558  ntrss2  13624  ntrin  13627  isopn3  13628  resttopon  13674  restuni2  13680  cnrest2r  13740  cnptopresti  13741  cnptoprest  13742  lmss  13749  metrest  14009  tgioo  14049  2sqlem8  14473  2sqlem9  14474  peano5set  14695