Theorem ssun1 3382

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 720	. . 3 |- ( x e. A -> ( x e. A \/ x e. B ) )
2		elun 3360	. . 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 3242	1 |- A C_ ( A u. B )

Syntax hints:   \/ wo 716   e. wcel 2203   u. cun 3209   C_ wss 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224

This theorem is referenced by:  ssun2  3383  ssun3  3384  elun1  3386  inabs  3453  reuun1  3503  un00  3555  undifabs  3586  undifss  3590  snsspr1  3842  snsstp1  3844  snsstp2  3845  prsstp12  3847  exmidundif  4319  sssucid  4536  unexb  4563  dmexg  5021  fvun1  5743  dftpos2  6492  tpostpos2  6496  mapunen  7104  ac6sfi  7155  caserel  7378  finomni  7431  ressxr  8317  nnssnn0  9499  un0addcl  9529  un0mulcl  9530  nn0ssxnn0  9566  hashfibclem  11206  ccatclab  11282  ccatrn  11297  fsumsplit  12093  fsum2d  12121  fsumabs  12151  fprodsplitdc  12282  fprod2d  12309  ennnfonelemss  13161  prdssca  13488  prdsbas  13489  prdsplusg  13490  prdsmulr  13491  lspun  14550  cnfldbas  14708  mpocnfldadd  14709  mpocnfldmul  14711  cnfldcj  14713  cnfldtset  14714  cnfldle  14715  cnfldds  14716  psrplusgg  14833  dvmptfsum  15590  elplyr  15605  lgsdir2lem3  15903  lgsquadlem2  15951  bdunexb  16690  gfsump1  16868  gfsumz  16869  gfsumcl  16870