Theorem p0ex 5320

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4761	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5243	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5316	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2828	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∅c0 4280  𝒫 cpw 4547  {csn 4573

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914  df-nul 4281  df-pw 4549  df-sn 4574

This theorem is referenced by:  pp0ex  5322  dtruALT  5324  zfpair  5357  tposexg  8170  fsetexb  8788  endisj  8977  pw2eng  8996  dfac4  10013  dfac2b  10022  axcc2lem  10327  axdc2lem  10339  axcclem  10348  axpowndlem3  10490  isstruct2  17060  cat1  18004  plusffval  18554  grpinvfval  18891  grpsubfval  18896  mulgfval  18982  0symgefmndeq  19306  staffval  20756  scaffval  20813  lpival  21261  ipffval  21585  refun0  23430  filconn  23798  alexsubALTlem2  23963  nmfval  24503  tcphex  25144  tchnmfval  25155  legval  28562  locfinref  33854  oms0  34310  bnj105  34736  ssoninhaus  36490  onint1  36491  bj-tagex  37029  bj-1uplex  37050  rrnval  37875  lsatset  39037  mnuprdlem2  44314  mnuprdlem3  44315  dvnprodlem3  45994  ioorrnopn  46351  ioorrnopnxr  46353  ismeannd  46513  nelsubc3  49111  setc1ohomfval  49533