Theorem pwuni 4781

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 4774	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		selpw 4460	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 235	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3893	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2081   ⊆ wss 3859  𝒫 cpw 4453  ∪ cuni 4745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866  df-ss 3874  df-pw 4455  df-uni 4746

This theorem is referenced by:  uniexr  7342  fipwuni  8736  uniwf  9094  rankuni  9138  rankc2  9146  rankxplim  9154  fin23lem17  9606  axcclem  9725  grurn  10069  istopon  21204  eltg3i  21253  cmpfi  21700  hmphdis  22088  ptcmpfi  22105  fbssfi  22129  mopnfss  22736  pliguhgr  27954  shsspwh  28714  circtopn  30718  hasheuni  30961  issgon  30999  sigaclci  31008  sigagenval  31016  dmsigagen  31020  imambfm  31137  salgenval  42148  salgenn0  42156  caragensspw  42333