Theorem pwuni 4896

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

Syntax hints:   ∈ wcel 2111   ⊆ wss 3902  𝒫 cpw 4550  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-pw 4552  df-uni 4860

This theorem is referenced by:  uniexr  7696  fipwuni  9310  uniwf  9709  rankuni  9753  rankc2  9761  rankxplim  9769  fin23lem17  10226  axcclem  10345  grurn  10689  istopon  22825  eltg3i  22874  cmpfi  23321  hmphdis  23709  ptcmpfi  23726  fbssfi  23750  mopnfss  24356  pliguhgr  30461  shsspwh  31221  circtopn  33845  hasheuni  34093  issgon  34131  sigaclci  34140  sigagenval  34148  dmsigagen  34152  imambfm  34270  bj-unirel  37084  salgenval  46358  salgenn0  46368  caragensspw  46546