Theorem pwuni 4905

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 4898	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4561	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 237	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3912	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867

This theorem is used by:  uniexr  7778  fipwuni  9422  uniwf  9832  rankuni  9883  rankc2  9892  rankxplim  9900  fin23lem17  10420  axcclem  10539  grurn  10890  istopon  23236  eltg3i  23285  cmpfi  23732  hmphdis  24121  ptcmpfi  24138  fbssfi  24162  mopnfss  24768  pliguhgr  31094  shsspwh  31854  circtopn  34516  hasheuni  34764  issgon  34802  sigaclci  34811  sigagenval  34820  dmsigagen  34824  imambfm  34941  bj-unirel  38059  salgenval  47425  salgenn0  47435  caragensspw  47613