Theorem pwuni 4944

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3950  𝒫 cpw 4599  ∪ cuni 4906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-pw 4601  df-uni 4907

This theorem is referenced by:  uniexr  7784  fipwuni  9467  uniwf  9860  rankuni  9904  rankc2  9912  rankxplim  9920  fin23lem17  10379  axcclem  10498  grurn  10842  istopon  22919  eltg3i  22969  cmpfi  23417  hmphdis  23805  ptcmpfi  23822  fbssfi  23846  mopnfss  24454  pliguhgr  30506  shsspwh  31266  circtopn  33837  hasheuni  34087  issgon  34125  sigaclci  34134  sigagenval  34142  dmsigagen  34146  imambfm  34265  bj-unirel  37053  salgenval  46341  salgenn0  46351  caragensspw  46529