Theorem inss1 3441

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

Syntax hints:   e. wcel 2203   i^i cin 3210   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224

This theorem is referenced by:  inss2  3442  ssinss1  3450  unabs  3452  inssddif  3462  inv1  3545  disjdif  3581  inundifss  3587  relin1  4870  resss  5062  resmpt3  5087  cnvcnvss  5217  funin  5427  funimass2  5434  fnresin1  5473  fnres  5475  fresin  5543  ssimaex  5738  fneqeql2  5787  fnfvimad  5922  isoini2  5992  ofrfval  6275  ofvalg  6276  ofrval  6277  off  6279  ofres  6281  ofco  6285  smores  6523  smores2  6525  tfrlem5  6545  pmresg  6910  unfiin  7186  infidc  7201  sbthlem7  7233  peano5nnnn  8207  peano5nni  9240  hashfibclem  11206  rexanuz  11673  nninfdclemcl  13199  nninfdclemp1  13201  fvsetsid  13246  tgvalex  13476  tgval2  14916  eltg3  14922  tgcl  14929  tgdom  14937  tgidm  14939  epttop  14955  ntropn  14982  ntrin  14989  cnptopresti  15103  cnptoprest  15104  txcnmpt  15138  xmetres  15247  metres  15248  blin2  15297  metrest  15371  tgioo  15419  limcresi  15531  2sqlem8  15996  bj-charfun  16577  bj-charfundc  16578  bj-charfundcALT  16579