Theorem pwuni 4926

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 4918	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4585	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 234	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3967	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2109   ⊆ wss 3931  𝒫 cpw 4580  ∪ cuni 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-pw 4582  df-uni 4889

This theorem is referenced by:  uniexr  7762  fipwuni  9443  uniwf  9838  rankuni  9882  rankc2  9890  rankxplim  9898  fin23lem17  10357  axcclem  10476  grurn  10820  istopon  22855  eltg3i  22904  cmpfi  23351  hmphdis  23739  ptcmpfi  23756  fbssfi  23780  mopnfss  24387  pliguhgr  30472  shsspwh  31232  circtopn  33873  hasheuni  34121  issgon  34159  sigaclci  34168  sigagenval  34176  dmsigagen  34180  imambfm  34299  bj-unirel  37074  salgenval  46330  salgenn0  46340  caragensspw  46518