Theorem inss1 3337

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 3300	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2	1	simplbi 272	. 2 |- ( x e. ( A i^i B ) -> x e. A )
3	2	ssriv 3141	1 |- ( A i^i B ) C_ A

Syntax hints:   e. wcel 2135   i^i cin 3110   C_ wss 3111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-in 3117  df-ss 3124

This theorem is referenced by:  inss2  3338  ssinss1  3346  unabs  3348  inssddif  3358  inv1  3440  disjdif  3476  inundifss  3481  relin1  4716  resss  4902  resmpt3  4927  cnvcnvss  5052  funin  5253  funimass2  5260  fnresin1  5296  fnres  5298  fresin  5360  ssimaex  5541  fneqeql2  5588  isoini2  5781  ofrfval  6052  ofvalg  6053  ofrval  6054  off  6056  ofres  6058  ofco  6062  smores  6251  smores2  6253  tfrlem5  6273  pmresg  6633  unfiin  6882  sbthlem7  6919  peano5nnnn  7824  peano5nni  8851  rexanuz  10916  nninfdclemcl  12320  nninfdclemp1  12322  fvsetsid  12365  tgvalex  12591  tgval2  12592  eltg3  12598  tgcl  12605  tgdom  12613  tgidm  12615  epttop  12631  ntropn  12658  ntrin  12665  cnptopresti  12779  cnptoprest  12780  txcnmpt  12814  xmetres  12923  metres  12924  blin2  12973  metrest  13047  tgioo  13087  limcresi  13176  bj-charfun  13524  bj-charfundc  13525  bj-charfundcALT  13526