Theorem p0ex 5287

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4747	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5213	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5283	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2912	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ∅c0 4293  𝒫 cpw 4541  {csn 4569

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 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294  df-pw 4543  df-sn 4570

This theorem is referenced by:  pp0ex  5289  dtruALT  5291  zfpair  5324  tposexg  7908  endisj  8606  pw2eng  8625  dfac4  9550  dfac2b  9558  axcc2lem  9860  axdc2lem  9872  axcclem  9881  axpowndlem3  10023  isstruct2  16495  plusffval  17860  grpinvfval  18144  grpsubfval  18149  mulgfval  18228  0symgefmndeq  18524  staffval  19620  scaffval  19654  lpival  20020  ipffval  20794  refun0  22125  filconn  22493  alexsubALTlem2  22658  nmfval  23200  tcphex  23822  tchnmfval  23833  legval  26372  locfinref  31107  oms0  31557  bnj105  31996  ssoninhaus  33798  onint1  33799  bj-tagex  34301  bj-1uplex  34322  rrnval  35107  lsatset  36128  mnuprdlem2  40616  mnuprdlem3  40617  dvnprodlem3  42240  ioorrnopn  42597  ioorrnopnxr  42599  ismeannd  42756