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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554  ∪ cuni 4863

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-pw 4556  df-uni 4864

This theorem is referenced by:  uniexr  7708  fipwuni  9329  uniwf  9731  rankuni  9775  rankc2  9783  rankxplim  9791  fin23lem17  10248  axcclem  10367  grurn  10712  istopon  22856  eltg3i  22905  cmpfi  23352  hmphdis  23740  ptcmpfi  23757  fbssfi  23781  mopnfss  24387  pliguhgr  30561  shsspwh  31321  circtopn  33994  hasheuni  34242  issgon  34280  sigaclci  34289  sigagenval  34297  dmsigagen  34301  imambfm  34419  bj-unirel  37252  salgenval  46561  salgenn0  46571  caragensspw  46749