Theorem pwuni 4950

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 4942	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4608	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 233	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3987	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949  𝒫 cpw 4603  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605  df-uni 4910

This theorem is referenced by:  uniexr  7750  fipwuni  9421  uniwf  9814  rankuni  9858  rankc2  9866  rankxplim  9874  fin23lem17  10333  axcclem  10452  grurn  10796  istopon  22414  eltg3i  22464  cmpfi  22912  hmphdis  23300  ptcmpfi  23317  fbssfi  23341  mopnfss  23949  pliguhgr  29739  shsspwh  30499  circtopn  32817  hasheuni  33083  issgon  33121  sigaclci  33130  sigagenval  33138  dmsigagen  33142  imambfm  33261  bj-unirel  35932  salgenval  45037  salgenn0  45047  caragensspw  45225