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  7763  fipwuni  9399  uniwf  9804  rankuni  9848  rankc2  9856  rankxplim  9864  fin23lem17  10343  axcclem  10462  grurn  10813  istopon  23140  eltg3i  23189  cmpfi  23636  hmphdis  24025  ptcmpfi  24042  fbssfi  24066  mopnfss  24672  pliguhgr  30970  shsspwh  31730  circtopn  34350  hasheuni  34598  issgon  34636  sigaclci  34645  sigagenval  34654  dmsigagen  34658  imambfm  34776  bj-unirel  37798  salgenval  47152  salgenn0  47162  caragensspw  47340