Theorem inss1 3451

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

This proof depends on syntax axioms:   e. wcel 2209   i^i cin 3219   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  inss2  3452  ssinss1  3460  unabs  3462  inssddif  3472  inv1  3559  vvin  3569  inundifss  3605  relin1  4897  resss  5089  resmpt3  5115  cnvcnvss  5245  funin  5455  funimass2  5462  fnresin1  5501  fnres  5503  fresin  5571  ssimaex  5767  fneqeql2  5821  fnfvimad  5957  isoini2  6028  ofrfval  6315  ofvalg  6316  ofrval  6317  off  6319  ofres  6321  ofco  6325  smores  6567  smores2  6569  tfrlem5  6589  pmresg  6961  unfiin  7237  infidc  7252  sbthlem7  7285  peano5nnnn  8265  peano5nni  9316  hashfibclem  11304  rexanuz  11776  nninfdclemcl  13397  nninfdclemp1  13399  fvsetsid  13444  tgvalex  13676  aspsubrg  15127  tgval2  15277  eltg3  15283  tgcl  15290  tgdom  15298  tgidm  15300  epttop  15316  ntropn  15343  ntrin  15350  cnptopresti  15464  cnptoprest  15465  txcnmpt  15499  xmetres  15608  metres  15609  blin2  15658  metrest  15732  tgioo  15780  limcresi  15892  ppiqsval  16240  ppiqfi  16242  ppiprm  16259  chtprm  16261  chtdif  16264  efchtqdvds  16265  ppidif  16269  prmorcht  16282  ppiqub  16293  2sqlem8  16447  bj-charfun  17038  bj-charfundc  17039  bj-charfundcALT  17040