Theorem pwuni 4877

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 4870	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4546	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 236	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3973	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2114   ⊆ wss 3938  𝒫 cpw 4541  ∪ cuni 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-pw 4543  df-uni 4841

This theorem is referenced by:  uniexr  7487  fipwuni  8892  uniwf  9250  rankuni  9294  rankc2  9302  rankxplim  9310  fin23lem17  9762  axcclem  9881  grurn  10225  istopon  21522  eltg3i  21571  cmpfi  22018  hmphdis  22406  ptcmpfi  22423  fbssfi  22447  mopnfss  23055  pliguhgr  28265  shsspwh  29025  circtopn  31103  hasheuni  31346  issgon  31384  sigaclci  31393  sigagenval  31401  dmsigagen  31405  imambfm  31522  bj-unirel  34346  salgenval  42613  salgenn0  42621  caragensspw  42798