Theorem pwuni 4878

Description: A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)

Assertion

Ref	Expression
pwuni	⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Proof of Theorem pwuni

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elssuni 4871	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4538	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3925	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2106   ⊆ wss 3887  𝒫 cpw 4533  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pw 4535  df-uni 4840

This theorem is referenced by:  uniexr  7613  fipwuni  9185  uniwf  9577  rankuni  9621  rankc2  9629  rankxplim  9637  fin23lem17  10094  axcclem  10213  grurn  10557  istopon  22061  eltg3i  22111  cmpfi  22559  hmphdis  22947  ptcmpfi  22964  fbssfi  22988  mopnfss  23596  pliguhgr  28848  shsspwh  29608  circtopn  31787  hasheuni  32053  issgon  32091  sigaclci  32100  sigagenval  32108  dmsigagen  32112  imambfm  32229  bj-unirel  35224  salgenval  43862  salgenn0  43870  caragensspw  44047