Theorem pwuni 4912

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-pw 4568  df-uni 4875

This theorem is referenced by:  uniexr  7742  fipwuni  9384  uniwf  9779  rankuni  9823  rankc2  9831  rankxplim  9839  fin23lem17  10298  axcclem  10417  grurn  10761  istopon  22806  eltg3i  22855  cmpfi  23302  hmphdis  23690  ptcmpfi  23707  fbssfi  23731  mopnfss  24338  pliguhgr  30422  shsspwh  31182  circtopn  33834  hasheuni  34082  issgon  34120  sigaclci  34129  sigagenval  34137  dmsigagen  34141  imambfm  34260  bj-unirel  37046  salgenval  46326  salgenn0  46336  caragensspw  46514