Theorem p0ex 5354

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  𝒫 cpw 4575  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943  df-nul 4309  df-pw 4577  df-sn 4602

This theorem is referenced by:  pp0ex  5356  dtruALT  5358  zfpair  5391  tposexg  8237  fsetexb  8876  endisj  9070  pw2eng  9090  dfac4  10134  dfac2b  10143  axcc2lem  10448  axdc2lem  10460  axcclem  10469  axpowndlem3  10611  isstruct2  17166  cat1  18108  plusffval  18622  grpinvfval  18959  grpsubfval  18964  mulgfval  19050  0symgefmndeq  19373  staffval  20799  scaffval  20835  lpival  21283  ipffval  21606  refun0  23451  filconn  23819  alexsubALTlem2  23984  nmfval  24525  tcphex  25167  tchnmfval  25178  legval  28509  locfinref  33818  oms0  34275  bnj105  34701  ssoninhaus  36412  onint1  36413  bj-tagex  36951  bj-1uplex  36972  rrnval  37797  lsatset  38954  mnuprdlem2  44245  mnuprdlem3  44246  dvnprodlem3  45925  ioorrnopn  46282  ioorrnopnxr  46284  ismeannd  46444  nelsubc3  48986  setc1ohomfval  49326