Theorem p0ex 5327

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5328. (Contributed by NM, 23-Dec-1993.)

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4766	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5250	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5323	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2831	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3438  ∅c0 4283  𝒫 cpw 4552  {csn 4578

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916  df-nul 4284  df-pw 4554  df-sn 4579

This theorem is referenced by:  pp0ex  5329  dtruALT  5331  zfpair  5364  tposexg  8180  fsetexb  8799  endisj  8990  pw2eng  9009  dfac4  10030  dfac2b  10039  axcc2lem  10344  axdc2lem  10356  axcclem  10365  axpowndlem3  10508  isstruct2  17074  cat1  18019  plusffval  18569  grpinvfval  18906  grpsubfval  18911  mulgfval  18997  0symgefmndeq  19321  staffval  20772  scaffval  20829  lpival  21277  ipffval  21601  refun0  23457  filconn  23825  alexsubALTlem2  23990  nmfval  24530  tcphex  25171  tchnmfval  25182  legval  28605  vieta  33685  locfinref  33947  oms0  34403  bnj105  34829  ssoninhaus  36591  onint1  36592  bj-tagex  37131  bj-1uplex  37152  rrnval  37967  lsatset  39189  mnuprdlem2  44456  mnuprdlem3  44457  dvnprodlem3  46134  ioorrnopn  46491  ioorrnopnxr  46493  ismeannd  46653  nelsubc3  49258  setc1ohomfval  49680