Theorem pwuni 4909

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565  df-uni 4872

This theorem is referenced by:  uniexr  7739  fipwuni  9377  uniwf  9772  rankuni  9816  rankc2  9824  rankxplim  9832  fin23lem17  10291  axcclem  10410  grurn  10754  istopon  22799  eltg3i  22848  cmpfi  23295  hmphdis  23683  ptcmpfi  23700  fbssfi  23724  mopnfss  24331  pliguhgr  30415  shsspwh  31175  circtopn  33827  hasheuni  34075  issgon  34113  sigaclci  34122  sigagenval  34130  dmsigagen  34134  imambfm  34253  bj-unirel  37039  salgenval  46319  salgenn0  46329  caragensspw  46507