Theorem pwuni 4901

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 4893	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4560	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3943	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2106   ⊆ wss 3905  𝒫 cpw 4555  ∪ cuni 4860

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3912  df-ss 3922  df-pw 4557  df-uni 4861

This theorem is referenced by:  uniexr  7684  fipwuni  9292  uniwf  9685  rankuni  9729  rankc2  9737  rankxplim  9745  fin23lem17  10204  axcclem  10323  grurn  10667  istopon  22171  eltg3i  22221  cmpfi  22669  hmphdis  23057  ptcmpfi  23074  fbssfi  23098  mopnfss  23706  pliguhgr  29202  shsspwh  29962  circtopn  32149  hasheuni  32415  issgon  32453  sigaclci  32462  sigagenval  32470  dmsigagen  32474  imambfm  32593  bj-unirel  35378  salgenval  44250  salgenn0  44258  caragensspw  44436