Theorem ssun1 2193

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 2173	. . 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 2069	1 |- A (_ (A u. B)

Syntax hints:   \/ wo 222   e. wcel 958   u. cun 2045   (_ wss 2047

This theorem is referenced by:  ssun2 2194  ssun3 2195  elun1 2197  inabs 2239  reuun1 2277  un00 2306  unexb 2873  sssucid 3047  dmexg 3358  asymref 3439  asymref2 3440  tfrlem11 3921  mapunen 4502  unifiOLD 4557  rankun 4691  cdadom3 4935  ressxr 5498  nnssnn0 6102  infxpidmlem1 7552  infxpidmlem11 7562  infunabs 7565  infdif 7568  psdmrn 8648  shsumval2 9360  sshhococ 9469

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053

Copyright terms: Public domain