Theorem pwuni 4903

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556  ∪ cuni 4865

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-pw 4558  df-uni 4866

This theorem is referenced by:  uniexr  7718  fipwuni  9341  uniwf  9743  rankuni  9787  rankc2  9795  rankxplim  9803  fin23lem17  10260  axcclem  10379  grurn  10724  istopon  22868  eltg3i  22917  cmpfi  23364  hmphdis  23752  ptcmpfi  23769  fbssfi  23793  mopnfss  24399  pliguhgr  30573  shsspwh  31333  circtopn  34014  hasheuni  34262  issgon  34300  sigaclci  34309  sigagenval  34317  dmsigagen  34321  imambfm  34439  bj-unirel  37293  salgenval  46673  salgenn0  46683  caragensspw  46861