Theorem inss1 3357

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

Syntax hints:   e. wcel 2148   i^i cin 3130   C_ wss 3131

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 2741  df-in 3137  df-ss 3144

This theorem is referenced by:  inss2  3358  ssinss1  3366  unabs  3368  inssddif  3378  inv1  3461  disjdif  3497  inundifss  3502  relin1  4746  resss  4933  resmpt3  4958  cnvcnvss  5085  funin  5289  funimass2  5296  fnresin1  5332  fnres  5334  fresin  5396  ssimaex  5579  fneqeql2  5627  isoini2  5822  ofrfval  6093  ofvalg  6094  ofrval  6095  off  6097  ofres  6099  ofco  6103  smores  6295  smores2  6297  tfrlem5  6317  pmresg  6678  unfiin  6927  sbthlem7  6964  peano5nnnn  7893  peano5nni  8924  rexanuz  10999  nninfdclemcl  12451  nninfdclemp1  12453  fvsetsid  12498  tgvalex  12717  tgval2  13636  eltg3  13642  tgcl  13649  tgdom  13657  tgidm  13659  epttop  13675  ntropn  13702  ntrin  13709  cnptopresti  13823  cnptoprest  13824  txcnmpt  13858  xmetres  13967  metres  13968  blin2  14017  metrest  14091  tgioo  14131  limcresi  14220  2sqlem8  14555  bj-charfun  14644  bj-charfundc  14645  bj-charfundcALT  14646