Theorem pwuni 4906

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559  df-uni 4868

This theorem is used by:  uniexr  7775  fipwuni  9411  uniwf  9821  rankuni  9872  rankc2  9881  rankxplim  9889  fin23lem17  10409  axcclem  10528  grurn  10879  istopon  23223  eltg3i  23272  cmpfi  23719  hmphdis  24108  ptcmpfi  24125  fbssfi  24149  mopnfss  24755  pliguhgr  31081  shsspwh  31841  circtopn  34462  hasheuni  34710  issgon  34748  sigaclci  34757  sigagenval  34766  dmsigagen  34770  imambfm  34887  bj-unirel  37946  salgenval  47300  salgenn0  47310  caragensspw  47488