Theorem pwuni 4969

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976  𝒫 cpw 4622  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-pw 4624  df-uni 4932

This theorem is referenced by:  uniexr  7798  fipwuni  9495  uniwf  9888  rankuni  9932  rankc2  9940  rankxplim  9948  fin23lem17  10407  axcclem  10526  grurn  10870  istopon  22939  eltg3i  22989  cmpfi  23437  hmphdis  23825  ptcmpfi  23842  fbssfi  23866  mopnfss  24474  pliguhgr  30518  shsspwh  31278  circtopn  33783  hasheuni  34049  issgon  34087  sigaclci  34096  sigagenval  34104  dmsigagen  34108  imambfm  34227  bj-unirel  37017  salgenval  46242  salgenn0  46252  caragensspw  46430