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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559  df-uni 4868

This theorem is used by:  uniexr  7762  fipwuni  9396  uniwf  9801  rankuni  9845  rankc2  9853  rankxplim  9861  fin23lem17  10340  axcclem  10459  grurn  10810  istopon  23137  eltg3i  23186  cmpfi  23633  hmphdis  24022  ptcmpfi  24039  fbssfi  24063  mopnfss  24669  pliguhgr  30967  shsspwh  31727  circtopn  34347  hasheuni  34595  issgon  34633  sigaclci  34642  sigagenval  34651  dmsigagen  34655  imambfm  34773  bj-unirel  37795  salgenval  47149  salgenn0  47159  caragensspw  47337