Theorem pwuni 4618

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 4611	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		selpw 4301	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 224	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3740	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2131   ⊆ wss 3707  𝒫 cpw 4294  ∪ cuni 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-in 3714  df-ss 3721  df-pw 4296  df-uni 4581

This theorem is referenced by:  uniexr  7129  fipwuni  8489  uniwf  8847  rankuni  8891  rankc2  8899  rankxplim  8907  fin23lem17  9344  axcclem  9463  grurn  9807  istopon  20911  eltg3i  20959  cmpfi  21405  hmphdis  21793  ptcmpfi  21810  fbssfi  21834  mopnfss  22441  pliguhgr  27641  shsspwh  28404  circtopn  30205  hasheuni  30448  issgon  30487  sigaclci  30496  sigagenval  30504  dmsigagen  30508  imambfm  30625  salgenval  41036  salgenn0  41044  caragensspw  41221