Theorem pwuni 4888

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 4881	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4546	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 234	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3925	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-pw 4543  df-uni 4851

This theorem is referenced by:  uniexr  7717  fipwuni  9339  uniwf  9743  rankuni  9787  rankc2  9795  rankxplim  9803  fin23lem17  10260  axcclem  10379  grurn  10724  istopon  22877  eltg3i  22926  cmpfi  23373  hmphdis  23761  ptcmpfi  23778  fbssfi  23802  mopnfss  24408  pliguhgr  30557  shsspwh  31317  circtopn  33981  hasheuni  34229  issgon  34267  sigaclci  34276  sigagenval  34284  dmsigagen  34288  imambfm  34406  bj-unirel  37358  salgenval  46749  salgenn0  46759  caragensspw  46937