Theorem p0ex 4984

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4478	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 4924	. . 3 ⊢ ∅ ∈ V
3	2	pwex 4979	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2847	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3351  ∅c0 4063  𝒫 cpw 4297  {csn 4316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-pw 4299  df-sn 4317

This theorem is referenced by:  pp0ex  4986  dtruALT  5027  zfpair  5032  opthprc  5307  snsn0non  5989  fvclex  7284  tposexg  7517  2dom  8181  endisj  8202  pw2eng  8221  dfac4  9144  dfac2b  9152  dfac2OLD  9154  cdaval  9193  axcc2lem  9459  axdc2lem  9471  axcclem  9480  axpowndlem3  9622  isstruct2  16073  plusffval  17454  staffval  19056  scaffval  19090  lpival  19459  ipffval  20209  refun0  21538  filconn  21906  alexsubALTlem2  22071  nmfval  22612  tchex  23234  tchnmfval  23245  legval  25699  locfinref  30245  oms0  30696  bnj105  31127  ssoninhaus  32781  onint1  32782  bj-tagex  33303  bj-1uplex  33324  rrnval  33954  lsatset  34795  dvnprodlem3  40677  ioorrnopn  41038  ioorrnopnxr  41040  ismeannd  41197