Theorem inss1 3476

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

Syntax hints:   e. wcel 1710   i^i cin 3209   C_ wss 3258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260

This theorem is referenced by:  inss2  3477  ssinss1  3484  unabs  3486  nssinpss  3488  dfin4  3496  inv1  3578  disjdif  3623  uniintsn  3964  pw1sspw  4172  inxpk  4278  cokrelk  4285  cnvkexg  4287  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  dfidk2  4314  peano5  4410  phialllem2  4618  resss  4989  funin  5164  funimass2  5171  fnresin1  5198  fnres  5200  isoini2  5499  clos1induct  5881  erdisj  5973  sbthlem1  6204