Theorem pwuni 4898

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553  ∪ cuni 4861

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 3440  df-ss 3922  df-pw 4555  df-uni 4862

This theorem is referenced by:  uniexr  7703  fipwuni  9335  uniwf  9734  rankuni  9778  rankc2  9786  rankxplim  9794  fin23lem17  10251  axcclem  10370  grurn  10714  istopon  22815  eltg3i  22864  cmpfi  23311  hmphdis  23699  ptcmpfi  23716  fbssfi  23740  mopnfss  24347  pliguhgr  30448  shsspwh  31208  circtopn  33803  hasheuni  34051  issgon  34089  sigaclci  34098  sigagenval  34106  dmsigagen  34110  imambfm  34229  bj-unirel  37024  salgenval  46303  salgenn0  46313  caragensspw  46491