Theorem inss1 3243

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 3206	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2	1	simplbi 270	. 2 |- ( x e. ( A i^i B ) -> x e. A )
3	2	ssriv 3051	1 |- ( A i^i B ) C_ A

Syntax hints:   e. wcel 1448   i^i cin 3020   C_ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-in 3027  df-ss 3034

This theorem is referenced by:  inss2  3244  ssinss1  3252  unabs  3254  inssddif  3264  inv1  3346  disjdif  3382  inundifss  3387  relin1  4595  resss  4779  resmpt3  4804  cnvcnvss  4929  funin  5130  funimass2  5137  fnresin1  5173  fnres  5175  fresin  5237  ssimaex  5414  fneqeql2  5461  isoini2  5652  ofrfval  5922  fnofval  5923  ofrval  5924  off  5926  ofres  5927  ofco  5931  smores  6119  smores2  6121  tfrlem5  6141  pmresg  6500  unfiin  6743  sbthlem7  6779  peano5nnnn  7577  peano5nni  8581  rexanuz  10600  fvsetsid  11775  tgvalex  12001  tgval2  12002  eltg3  12008  tgcl  12015  tgdom  12023  tgidm  12025  epttop  12041  ntropn  12068  ntrin  12075  cnptopresti  12188  cnptoprest  12189  txcnmpt  12223  xmetres  12310  metres  12311  blin2  12360  metrest  12434  tgioo  12465  limcresi  12515