Theorem pwuni 4898

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 4891	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4556	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 234	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3935	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2113   ⊆ wss 3899  𝒫 cpw 4551  ∪ cuni 4860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-ss 3916  df-pw 4553  df-uni 4861

This theorem is referenced by:  uniexr  7705  fipwuni  9320  uniwf  9722  rankuni  9766  rankc2  9774  rankxplim  9782  fin23lem17  10239  axcclem  10358  grurn  10702  istopon  22837  eltg3i  22886  cmpfi  23333  hmphdis  23721  ptcmpfi  23738  fbssfi  23762  mopnfss  24368  pliguhgr  30477  shsspwh  31237  circtopn  33861  hasheuni  34109  issgon  34147  sigaclci  34156  sigagenval  34164  dmsigagen  34168  imambfm  34286  bj-unirel  37106  salgenval  46433  salgenn0  46443  caragensspw  46621