Theorem ssun1 3427

Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ssun1	|- A C_ (A u. B)

Proof of Theorem ssun1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orc 374	. . 3 |- (x e. A -> (x e. A \/ x e. B))
2		elun 3221	. . 3 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
3	1, 2	sylibr 203	. 2 |- (x e. A -> x e. (A u. B))
4	3	ssriv 3278	1 |- A C_ (A u. B)

Syntax hints:   \/ wo 357   e. wcel 1710   u. cun 3208   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-un 3215  df-ss 3260

This theorem is referenced by:  ssun2  3428  ssun3  3429  elun1  3431  inabs  3487  reuun1  3538  un00  3587  snsspr1  3857  snsstp1  3859  snsstp2  3860  uniintsn  3964  snprss1  4121  pw1equn  4332  pw1eqadj  4333  evenoddnnnul  4515  sfinltfin  4536  vfinspsslem1  4551  vfinspss  4552  phi011lem1  4599  enadjlem1  6060  ncdisjun  6137  ce0addcnnul  6180  addlec  6209