Theorem pwuni 4883

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 4876	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
2		velpw 4541	. . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴)
3	1, 2	sylibr 235	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴)
4	3	ssriv 3926	1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴

Syntax hints:   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-pw 4538  df-uni 4846

This theorem is referenced by:  uniexr  7713  fipwuni  9336  uniwf  9741  rankuni  9785  rankc2  9793  rankxplim  9801  fin23lem17  10258  axcclem  10377  grurn  10722  istopon  22902  eltg3i  22951  cmpfi  23398  hmphdis  23786  ptcmpfi  23803  fbssfi  23827  mopnfss  24433  pliguhgr  30582  shsspwh  31342  circtopn  34028  hasheuni  34276  issgon  34314  sigaclci  34323  sigagenval  34331  dmsigagen  34335  imambfm  34453  bj-unirel  37411  salgenval  46771  salgenn0  46781  caragensspw  46959