Theorem inss1 3429

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 3392	. . 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 3232	1 |- ( A i^i B ) C_ A

Syntax hints:   e. wcel 2202   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:  inss2  3430  ssinss1  3438  unabs  3440  inssddif  3450  inv1  3533  disjdif  3569  inundifss  3574  relin1  4851  resss  5043  resmpt3  5068  cnvcnvss  5198  funin  5408  funimass2  5415  fnresin1  5454  fnres  5456  fresin  5523  ssimaex  5716  fneqeql2  5765  fnfvimad  5900  isoini2  5970  ofrfval  6253  ofvalg  6254  ofrval  6255  off  6257  ofres  6259  ofco  6263  smores  6501  smores2  6503  tfrlem5  6523  pmresg  6888  unfiin  7161  infidc  7176  sbthlem7  7205  peano5nnnn  8172  peano5nni  9205  rexanuz  11628  nninfdclemcl  13149  nninfdclemp1  13151  fvsetsid  13196  tgvalex  13426  tgval2  14862  eltg3  14868  tgcl  14875  tgdom  14883  tgidm  14885  epttop  14901  ntropn  14928  ntrin  14935  cnptopresti  15049  cnptoprest  15050  txcnmpt  15084  xmetres  15193  metres  15194  blin2  15243  metrest  15317  tgioo  15365  limcresi  15477  2sqlem8  15942  bj-charfun  16523  bj-charfundc  16524  bj-charfundcALT  16525