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 4557	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 236	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3938	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2141   ⊆ wss 3902  𝒫 cpw 4552  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-pw 4554  df-uni 4863

This theorem is referenced by:  uniexr  7741  fipwuni  9366  uniwf  9771  rankuni  9815  rankc2  9823  rankxplim  9831  fin23lem17  10289  axcclem  10408  grurn  10753  istopon  22960  eltg3i  23009  cmpfi  23456  hmphdis  23844  ptcmpfi  23861  fbssfi  23885  mopnfss  24491  pliguhgr  30646  shsspwh  31406  circtopn  34095  hasheuni  34343  issgon  34381  sigaclci  34390  sigagenval  34398  dmsigagen  34402  imambfm  34520  bj-unirel  37497  salgenval  46856  salgenn0  46866  caragensspw  47044