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

Syntax hints:   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4564  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4566  df-uni 4874

This theorem is referenced by:  uniexr  7758  fipwuni  9382  uniwf  9787  rankuni  9831  rankc2  9839  rankxplim  9847  fin23lem17  10318  axcclem  10437  grurn  10782  istopon  23034  eltg3i  23083  cmpfi  23530  hmphdis  23918  ptcmpfi  23935  fbssfi  23959  mopnfss  24565  pliguhgr  30775  shsspwh  31535  circtopn  34168  hasheuni  34416  issgon  34454  sigaclci  34463  sigagenval  34471  dmsigagen  34475  imambfm  34593  bj-unirel  37571  salgenval  46920  salgenn0  46930  caragensspw  47108