Theorem ssun1 3323

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 3301	. . 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 3184	1 |- A C_ ( A u. B )

Syntax hints:   \/ wo 709   e. wcel 2164   u. cun 3152   C_ wss 3154

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 3158  df-in 3160  df-ss 3167

This theorem is referenced by:  ssun2  3324  ssun3  3325  elun1  3327  inabs  3392  reuun1  3442  un00  3494  undifabs  3524  undifss  3528  snsspr1  3767  snsstp1  3769  snsstp2  3770  prsstp12  3772  exmidundif  4236  sssucid  4447  unexb  4474  dmexg  4927  fvun1  5624  dftpos2  6316  tpostpos2  6320  ac6sfi  6956  caserel  7148  finomni  7201  ressxr  8065  nnssnn0  9246  un0addcl  9276  un0mulcl  9277  nn0ssxnn0  9309  fsumsplit  11553  fsum2d  11581  fsumabs  11611  fprodsplitdc  11742  fprod2d  11769  ennnfonelemss  12570  lspun  13901  cnfldbas  14059  mpocnfldadd  14060  mpocnfldmul  14062  cnfldcj  14064  cnfldtset  14065  cnfldle  14066  cnfldds  14067  psrplusgg  14173  dvmptfsum  14904  elplyr  14919  lgsdir2lem3  15187  lgsquadlem2  15235  bdunexb  15482