Theorem pwuni 4896

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898  𝒫 cpw 4549  ∪ cuni 4858

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 3439  df-ss 3915  df-pw 4551  df-uni 4859

This theorem is referenced by:  uniexr  7702  fipwuni  9317  uniwf  9719  rankuni  9763  rankc2  9771  rankxplim  9779  fin23lem17  10236  axcclem  10355  grurn  10699  istopon  22828  eltg3i  22877  cmpfi  23324  hmphdis  23712  ptcmpfi  23729  fbssfi  23753  mopnfss  24359  pliguhgr  30468  shsspwh  31228  circtopn  33871  hasheuni  34119  issgon  34157  sigaclci  34166  sigagenval  34174  dmsigagen  34178  imambfm  34296  bj-unirel  37116  salgenval  46443  salgenn0  46453  caragensspw  46631