Theorem inss1 3347

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

Syntax hints:   e. wcel 2141   i^i cin 3120   C_ wss 3121

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  inss2  3348  ssinss1  3356  unabs  3358  inssddif  3368  inv1  3451  disjdif  3487  inundifss  3492  relin1  4729  resss  4915  resmpt3  4940  cnvcnvss  5065  funin  5269  funimass2  5276  fnresin1  5312  fnres  5314  fresin  5376  ssimaex  5557  fneqeql2  5605  isoini2  5798  ofrfval  6069  ofvalg  6070  ofrval  6071  off  6073  ofres  6075  ofco  6079  smores  6271  smores2  6273  tfrlem5  6293  pmresg  6654  unfiin  6903  sbthlem7  6940  peano5nnnn  7854  peano5nni  8881  rexanuz  10952  nninfdclemcl  12403  nninfdclemp1  12405  fvsetsid  12450  tgvalex  12844  tgval2  12845  eltg3  12851  tgcl  12858  tgdom  12866  tgidm  12868  epttop  12884  ntropn  12911  ntrin  12918  cnptopresti  13032  cnptoprest  13033  txcnmpt  13067  xmetres  13176  metres  13177  blin2  13226  metrest  13300  tgioo  13340  limcresi  13429  2sqlem8  13753  bj-charfun  13842  bj-charfundc  13843  bj-charfundcALT  13844