Theorem pwuni 4825

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 4403	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		selpw 4115	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 223	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3572	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373

This theorem is referenced by:  uniexb  6866  fipwuni  8215  uniwf  8565  rankuni  8609  rankc2  8617  rankxplim  8625  fin23lem17  9043  axcclem  9162  grurn  9502  istopon  20540  eltg3i  20576  cmpfi  21021  hmphdis  21409  ptcmpfi  21426  fbssfi  21451  mopnfss  22058  shsspwh  27487  circtopn  29232  hasheuni  29474  issgon  29513  sigaclci  29522  sigagenval  29530  dmsigagen  29534  imambfm  29651  salgenval  39217  salgenn0  39225  caragensspw  39399