Theorem ssun1 3322

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 713	. . 3 |- ( x e. A -> ( x e. A \/ x e. B ) )
2		elun 3300	. . 3 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
3	1, 2	sylibr 134	. 2 |- ( x e. A -> x e. ( A u. B ) )
4	3	ssriv 3183	1 |- A C_ ( A u. B )

Syntax hints:   \/ wo 709   e. wcel 2164   u. cun 3151   C_ wss 3153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-in 3159  df-ss 3166

This theorem is referenced by:  ssun2  3323  ssun3  3324  elun1  3326  inabs  3391  reuun1  3441  un00  3493  undifabs  3523  undifss  3527  snsspr1  3766  snsstp1  3768  snsstp2  3769  prsstp12  3771  exmidundif  4235  sssucid  4446  unexb  4473  dmexg  4926  fvun1  5623  dftpos2  6314  tpostpos2  6318  ac6sfi  6954  caserel  7146  finomni  7199  ressxr  8063  nnssnn0  9243  un0addcl  9273  un0mulcl  9274  nn0ssxnn0  9306  fsumsplit  11550  fsum2d  11578  fsumabs  11608  fprodsplitdc  11739  fprod2d  11766  ennnfonelemss  12567  lspun  13898  cnfldbas  14051  cnfldadd  14052  cnfldmul  14054  psrplusgg  14162  elplyr  14886  lgsdir2lem3  15146  bdunexb  15412