Theorem inss1 3355

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
inss1	|- ( A i^i B ) C_ A

Proof of Theorem inss1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3318	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2	1	simplbi 274	. 2 |- ( x e. ( A i^i B ) -> x e. A )
3	2	ssriv 3159	1 |- ( A i^i B ) C_ A

Syntax hints:   e. wcel 2148   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:  inss2  3356  ssinss1  3364  unabs  3366  inssddif  3376  inv1  3459  disjdif  3495  inundifss  3500  relin1  4742  resss  4928  resmpt3  4953  cnvcnvss  5080  funin  5284  funimass2  5291  fnresin1  5327  fnres  5329  fresin  5391  ssimaex  5574  fneqeql2  5622  isoini2  5815  ofrfval  6086  ofvalg  6087  ofrval  6088  off  6090  ofres  6092  ofco  6096  smores  6288  smores2  6290  tfrlem5  6310  pmresg  6671  unfiin  6920  sbthlem7  6957  peano5nnnn  7886  peano5nni  8916  rexanuz  10988  nninfdclemcl  12439  nninfdclemp1  12441  fvsetsid  12486  tgvalex  13332  tgval2  13333  eltg3  13339  tgcl  13346  tgdom  13354  tgidm  13356  epttop  13372  ntropn  13399  ntrin  13406  cnptopresti  13520  cnptoprest  13521  txcnmpt  13555  xmetres  13664  metres  13665  blin2  13714  metrest  13788  tgioo  13828  limcresi  13917  2sqlem8  14241  bj-charfun  14330  bj-charfundc  14331  bj-charfundcALT  14332