Theorem inss1 3393

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

Syntax hints:   e. wcel 2176   i^i cin 3165   C_ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  inss2  3394  ssinss1  3402  unabs  3404  inssddif  3414  inv1  3497  disjdif  3533  inundifss  3538  relin1  4794  resss  4984  resmpt3  5009  cnvcnvss  5138  funin  5346  funimass2  5353  fnresin1  5392  fnres  5394  fresin  5456  ssimaex  5642  fneqeql2  5691  isoini2  5890  ofrfval  6169  ofvalg  6170  ofrval  6171  off  6173  ofres  6175  ofco  6179  smores  6380  smores2  6382  tfrlem5  6402  pmresg  6765  unfiin  7025  infidc  7038  sbthlem7  7067  peano5nnnn  8007  peano5nni  9041  rexanuz  11332  nninfdclemcl  12852  nninfdclemp1  12854  fvsetsid  12899  tgvalex  13128  tgval2  14556  eltg3  14562  tgcl  14569  tgdom  14577  tgidm  14579  epttop  14595  ntropn  14622  ntrin  14629  cnptopresti  14743  cnptoprest  14744  txcnmpt  14778  xmetres  14887  metres  14888  blin2  14937  metrest  15011  tgioo  15059  limcresi  15171  2sqlem8  15633  bj-charfun  15780  bj-charfundc  15781  bj-charfundcALT  15782