Theorem pwuni 4889

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-pw 4544  df-uni 4852

This theorem is referenced by:  uniexr  7710  fipwuni  9332  uniwf  9734  rankuni  9778  rankc2  9786  rankxplim  9794  fin23lem17  10251  axcclem  10370  grurn  10715  istopon  22887  eltg3i  22936  cmpfi  23383  hmphdis  23771  ptcmpfi  23788  fbssfi  23812  mopnfss  24418  pliguhgr  30572  shsspwh  31332  circtopn  33997  hasheuni  34245  issgon  34283  sigaclci  34292  sigagenval  34300  dmsigagen  34304  imambfm  34422  bj-unirel  37374  salgenval  46767  salgenn0  46777  caragensspw  46955