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  3450  disjdif  3486  inundifss  3491  relin1  4727  resss  4913  resmpt3  4938  cnvcnvss  5063  funin  5267  funimass2  5274  fnresin1  5310  fnres  5312  fresin  5374  ssimaex  5555  fneqeql2  5602  isoini2  5795  ofrfval  6066  ofvalg  6067  ofrval  6068  off  6070  ofres  6072  ofco  6076  smores  6268  smores2  6270  tfrlem5  6290  pmresg  6650  unfiin  6899  sbthlem7  6936  peano5nnnn  7841  peano5nni  8868  rexanuz  10939  nninfdclemcl  12390  nninfdclemp1  12392  fvsetsid  12437  tgvalex  12803  tgval2  12804  eltg3  12810  tgcl  12817  tgdom  12825  tgidm  12827  epttop  12843  ntropn  12870  ntrin  12877  cnptopresti  12991  cnptoprest  12992  txcnmpt  13026  xmetres  13135  metres  13136  blin2  13185  metrest  13259  tgioo  13299  limcresi  13388  2sqlem8  13712  bj-charfun  13802  bj-charfundc  13803  bj-charfundcALT  13804