Theorem inss2 3356

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 3327	. 2 |- ( B i^i A ) = ( A i^i B )
2		inss1 3355	. 2 |- ( B i^i A ) C_ B
3	1, 2	eqsstrri 3188	1 |- ( A i^i B ) C_ B

Syntax hints:   i^i cin 3128   C_ wss 3129

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 2739  df-in 3135  df-ss 3142

This theorem is referenced by:  difin0  3496  bnd2  4171  ordin  4383  relin2  4743  relres  4932  ssrnres  5068  cnvcnv  5078  funinsn  5262  funimaexg  5297  fnresin2  5328  ssimaex  5574  ffvresb  5676  ofrfval  6086  ofvalg  6087  ofrval  6088  off  6090  ofres  6092  ofco  6096  offres  6131  tpostpos  6260  smores3  6289  tfrlem5  6310  tfrexlem  6330  erinxp  6604  pmresg  6671  unfiin  6920  ltrelpi  7318  peano5nnnn  7886  peano5nni  8916  rexanuz  10988  structcnvcnv  12468  ressbasssd  12519  restsspw  12684  eltg4i  13337  ntrss2  13403  ntrin  13406  isopn3  13407  resttopon  13453  restuni2  13459  cnrest2r  13519  cnptopresti  13520  cnptoprest  13521  lmss  13528  metrest  13788  tgioo  13828  2sqlem8  14241  2sqlem9  14242  peano5set  14463