Theorem ssun1 2189

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

Assertion

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

Proof of Theorem ssun1

Step	Hyp	Ref	Expression
1		orc 269	. . 3 |- (x e. A -> (x e. A \/ x e. B))
2		elun 2169	. . 3 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
3	1, 2	sylibr 200	. 2 |- (x e. A -> x e. (A u. B))
4	3	ssriv 2065	1 |- A (_ (A u. B)

Syntax hints:   \/ wo 222   e. wcel 956   u. cun 2041   (_ wss 2043

This theorem is referenced by:  ssun2 2190  ssun3 2191  elun1 2193  inabs 2235  reuun1 2273  un00 2302  unexb 2868  sssucid 3042  dmexg 3352  asymref 3431  asymref2 3432  tfrlem11 3912  mapunen 4488  unifi 4538  rankun 4671  cdadom3 4915  ressxr 5478  nnssnn0 6057  infxpidmlem1 7503  infxpidmlem11 7513  infunabs 7516  infdif 7519  psdmrn 8591  shsumval2 9298  sshhococ 9407

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-in 2047  df-ss 2049

Copyright terms: Public domain