Theorem pwuni 4948

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

Syntax hints:   ∈ wcel 2098   ⊆ wss 3945  𝒫 cpw 4603  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-ss 3962  df-pw 4605  df-uni 4909

This theorem is referenced by:  uniexr  7764  fipwuni  9449  uniwf  9842  rankuni  9886  rankc2  9894  rankxplim  9902  fin23lem17  10361  axcclem  10480  grurn  10824  istopon  22845  eltg3i  22895  cmpfi  23343  hmphdis  23731  ptcmpfi  23748  fbssfi  23772  mopnfss  24380  pliguhgr  30353  shsspwh  31113  circtopn  33525  hasheuni  33791  issgon  33829  sigaclci  33838  sigagenval  33846  dmsigagen  33850  imambfm  33969  bj-unirel  36617  salgenval  45789  salgenn0  45799  caragensspw  45977