Theorem pwuni 4875

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3936  𝒫 cpw 4539  ∪ cuni 4838

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-pw 4541  df-uni 4839

This theorem is referenced by:  uniexr  7485  fipwuni  8890  uniwf  9248  rankuni  9292  rankc2  9300  rankxplim  9308  fin23lem17  9760  axcclem  9879  grurn  10223  istopon  21520  eltg3i  21569  cmpfi  22016  hmphdis  22404  ptcmpfi  22421  fbssfi  22445  mopnfss  23053  pliguhgr  28263  shsspwh  29023  circtopn  31101  hasheuni  31344  issgon  31382  sigaclci  31391  sigagenval  31399  dmsigagen  31403  imambfm  31520  bj-unirel  34347  salgenval  42626  salgenn0  42634  caragensspw  42811