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	⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Proof of Theorem ssun1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		orc 720	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
2		elun 3360	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
3	1, 2	sylibr 134	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∪ 𝐵))
4	3	ssriv 3242	1 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 716   ∈ wcel 2203   ∪ cun 3209   ⊆ 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  11204  ccatclab  11280  ccatrn  11295  fsumsplit  12091  fsum2d  12119  fsumabs  12149  fprodsplitdc  12280  fprod2d  12307  ennnfonelemss  13159  prdssca  13486  prdsbas  13487  prdsplusg  13488  prdsmulr  13489  lspun  14548  cnfldbas  14706  mpocnfldadd  14707  mpocnfldmul  14709  cnfldcj  14711  cnfldtset  14712  cnfldle  14713  cnfldds  14714  psrplusgg  14831  dvmptfsum  15588  elplyr  15603  lgsdir2lem3  15901  lgsquadlem2  15949  bdunexb  16688  gfsump1  16866  gfsumz  16867  gfsumcl  16868