Theorem pwuni 4858

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 4851	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4518	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 237	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3905	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2110   ⊆ wss 3866  𝒫 cpw 4513  ∪ cuni 4819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-pw 4515  df-uni 4820

This theorem is referenced by:  uniexr  7548  fipwuni  9042  uniwf  9435  rankuni  9479  rankc2  9487  rankxplim  9495  fin23lem17  9952  axcclem  10071  grurn  10415  istopon  21809  eltg3i  21858  cmpfi  22305  hmphdis  22693  ptcmpfi  22710  fbssfi  22734  mopnfss  23341  pliguhgr  28567  shsspwh  29327  circtopn  31501  hasheuni  31765  issgon  31803  sigaclci  31812  sigagenval  31820  dmsigagen  31824  imambfm  31941  bj-unirel  34961  salgenval  43537  salgenn0  43545  caragensspw  43722