Theorem p0ex 5310

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4750	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5234	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5306	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2837	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3430  ∅c0 4261  𝒫 cpw 4538  {csn 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-dif 3894  df-in 3898  df-ss 3908  df-nul 4262  df-pw 4540  df-sn 4567

This theorem is referenced by:  pp0ex  5312  dtruALT  5314  zfpair  5347  tposexg  8040  fsetexb  8626  endisj  8815  pw2eng  8834  dfac4  9862  dfac2b  9870  axcc2lem  10176  axdc2lem  10188  axcclem  10197  axpowndlem3  10339  isstruct2  16831  cat1  17793  plusffval  18313  grpinvfval  18599  grpsubfval  18604  mulgfval  18683  0symgefmndeq  18982  staffval  20088  scaffval  20122  lpival  20497  ipffval  20834  refun0  22647  filconn  23015  alexsubALTlem2  23180  nmfval  23725  tcphex  24362  tchnmfval  24373  legval  26926  locfinref  31770  oms0  32243  bnj105  32682  ssoninhaus  34616  onint1  34617  bj-tagex  35156  bj-1uplex  35177  rrnval  35964  lsatset  36983  mnuprdlem2  41844  mnuprdlem3  41845  dvnprodlem3  43443  ioorrnopn  43800  ioorrnopnxr  43802  ismeannd  43959