Theorem pwuni 4875

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532  df-uni 4837

This theorem is referenced by:  uniexr  7591  fipwuni  9115  uniwf  9508  rankuni  9552  rankc2  9560  rankxplim  9568  fin23lem17  10025  axcclem  10144  grurn  10488  istopon  21969  eltg3i  22019  cmpfi  22467  hmphdis  22855  ptcmpfi  22872  fbssfi  22896  mopnfss  23504  pliguhgr  28749  shsspwh  29509  circtopn  31689  hasheuni  31953  issgon  31991  sigaclci  32000  sigagenval  32008  dmsigagen  32012  imambfm  32129  bj-unirel  35151  salgenval  43752  salgenn0  43760  caragensspw  43937