Theorem inss1 3356

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

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

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 2740  df-in 3136  df-ss 3143

This theorem is referenced by:  inss2  3357  ssinss1  3365  unabs  3367  inssddif  3377  inv1  3460  disjdif  3496  inundifss  3501  relin1  4745  resss  4932  resmpt3  4957  cnvcnvss  5084  funin  5288  funimass2  5295  fnresin1  5331  fnres  5333  fresin  5395  ssimaex  5578  fneqeql2  5626  isoini2  5820  ofrfval  6091  ofvalg  6092  ofrval  6093  off  6095  ofres  6097  ofco  6101  smores  6293  smores2  6295  tfrlem5  6315  pmresg  6676  unfiin  6925  sbthlem7  6962  peano5nnnn  7891  peano5nni  8922  rexanuz  10997  nninfdclemcl  12449  nninfdclemp1  12451  fvsetsid  12496  tgvalex  12712  tgval2  13554  eltg3  13560  tgcl  13567  tgdom  13575  tgidm  13577  epttop  13593  ntropn  13620  ntrin  13627  cnptopresti  13741  cnptoprest  13742  txcnmpt  13776  xmetres  13885  metres  13886  blin2  13935  metrest  14009  tgioo  14049  limcresi  14138  2sqlem8  14473  bj-charfun  14562  bj-charfundc  14563  bj-charfundcALT  14564