Theorem ssun1 2204

Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27.

Assertion

Ref	Expression
ssun1	⊢ A ⊆ (A ∪ B)

Proof of Theorem ssun1

Step	Hyp	Ref	Expression
1		orc 269	. . 3 ⊢ (x ∈ A → (x ∈ A ⋁ x ∈ B))
2		elun 2184	. . 3 ⊢ (x ∈ (A ∪ B) ↔ (x ∈ A ⋁ x ∈ B))
3	1, 2	sylibr 200	. 2 ⊢ (x ∈ A → x ∈ (A ∪ B))
4	3	ssriv 2080	1 ⊢ A ⊆ (A ∪ B)

Syntax hints:   ⋁ wo 222   ∈ wcel 962   ∪ cun 2056   ⊆ wss 2058

This theorem is referenced by:  ssun2 2205  ssun3 2206  elun1 2208  inabs 2250  reuun1 2288  un00 2318  unexb 2889  sssucid 3063  dmexg 3374  asymref 3455  asymref2 3456  tfrlem11 3937  mapunen 4522  unifi 4573  rankun 4708  cdadom3 4955  ressxr 5518  nnssnn0 6134  infxpidmlem1 7585  infxpidmlem11 7595  infunabs 7598  infdif 7601  psdmrn 8673  shsumval2i 9384  sshhococi 9493

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-clab 1470  df-cleq 1475  df-clel 1478  df-v 1819  df-un 2061  df-in 2062  df-ss 2064

Copyright terms: Public domain