Theorem inss1 3426

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

Syntax hints:   e. wcel 2201   i^i cin 3198   C_ wss 3199

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-in 3205  df-ss 3212

This theorem is referenced by:  inss2  3427  ssinss1  3435  unabs  3437  inssddif  3447  inv1  3530  disjdif  3566  inundifss  3571  relin1  4847  resss  5039  resmpt3  5064  cnvcnvss  5193  funin  5403  funimass2  5410  fnresin1  5449  fnres  5451  fresin  5517  ssimaex  5710  fneqeql2  5759  fnfvimad  5895  isoini2  5965  ofrfval  6249  ofvalg  6250  ofrval  6251  off  6253  ofres  6255  ofco  6259  smores  6463  smores2  6465  tfrlem5  6485  pmresg  6850  unfiin  7123  infidc  7138  sbthlem7  7167  peano5nnnn  8117  peano5nni  9151  rexanuz  11571  nninfdclemcl  13092  nninfdclemp1  13094  fvsetsid  13139  tgvalex  13369  tgval2  14804  eltg3  14810  tgcl  14817  tgdom  14825  tgidm  14827  epttop  14843  ntropn  14870  ntrin  14877  cnptopresti  14991  cnptoprest  14992  txcnmpt  15026  xmetres  15135  metres  15136  blin2  15185  metrest  15259  tgioo  15307  limcresi  15419  2sqlem8  15881  bj-charfun  16462  bj-charfundc  16463  bj-charfundcALT  16464