Theorem pwuni 4950

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3963  𝒫 cpw 4605  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-pw 4607  df-uni 4913

This theorem is referenced by:  uniexr  7782  fipwuni  9464  uniwf  9857  rankuni  9901  rankc2  9909  rankxplim  9917  fin23lem17  10376  axcclem  10495  grurn  10839  istopon  22934  eltg3i  22984  cmpfi  23432  hmphdis  23820  ptcmpfi  23837  fbssfi  23861  mopnfss  24469  pliguhgr  30515  shsspwh  31275  circtopn  33798  hasheuni  34066  issgon  34104  sigaclci  34113  sigagenval  34121  dmsigagen  34125  imambfm  34244  bj-unirel  37034  salgenval  46277  salgenn0  46287  caragensspw  46465