Theorem pwuni 4912

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 4905	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4568	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 237	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3942	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906  𝒫 cpw 4563  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-pw 4565  df-uni 4874

This theorem is referenced by:  uniexr  7763  fipwuni  9387  uniwf  9792  rankuni  9836  rankc2  9844  rankxplim  9852  fin23lem17  10323  axcclem  10442  grurn  10787  istopon  23050  eltg3i  23099  cmpfi  23546  hmphdis  23934  ptcmpfi  23951  fbssfi  23975  mopnfss  24581  pliguhgr  30819  shsspwh  31579  circtopn  34208  hasheuni  34456  issgon  34494  sigaclci  34503  sigagenval  34511  dmsigagen  34515  imambfm  34633  bj-unirel  37668  salgenval  47018  salgenn0  47028  caragensspw  47206