Theorem p0ex 5356

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4782	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5272	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5352	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2866	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  𝒫 cpw 4567  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930  df-nul 4295  df-pw 4569  df-sn 4595

This theorem is referenced by:  pp0ex  5358  dtruALT  5360  zfpair  5393  tposexg  8235  fsetexb  8860  endisj  9051  pw2eng  9070  dfac4  10105  dfac2b  10113  axcc2lem  10419  axdc2lem  10431  axcclem  10440  axpowndlem3  10583  isstruct2  17208  cat1  18153  plusffval  18703  grpinvfval  19044  grpsubfval  19049  mulgfval  19134  0symgefmndeq  19463  staffval  20921  scaffval  20978  ipffval  21766  refun0  23640  filconn  24008  alexsubALTlem2  24173  nmfval  24713  tcphex  25344  tchnmfval  25355  legval  28818  vieta  33914  locfinref  34175  oms0  34631  bnj105  35057  ssoninhaus  36847  onint1  36848  bj-tagex  37510  bj-1uplex  37531  rrnval  38365  dvnprodlem3  46553  ioorrnopn  46910  ioorrnopnxr  46912  ismeannd  47072  nelsubc3  49733  setc1ohomfval  50155