Theorem p0ex 5331

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4770	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5254	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5327	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2834	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  𝒫 cpw 4556  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920  df-nul 4288  df-pw 4558  df-sn 4583

This theorem is referenced by:  pp0ex  5333  dtruALT  5335  zfpair  5368  tposexg  8192  fsetexb  8813  endisj  9004  pw2eng  9023  dfac4  10044  dfac2b  10053  axcc2lem  10358  axdc2lem  10370  axcclem  10379  axpowndlem3  10522  isstruct2  17088  cat1  18033  plusffval  18583  grpinvfval  18920  grpsubfval  18925  mulgfval  19011  0symgefmndeq  19335  staffval  20786  scaffval  20843  lpival  21291  ipffval  21615  refun0  23471  filconn  23839  alexsubALTlem2  24004  nmfval  24544  tcphex  25185  tchnmfval  25196  legval  28668  vieta  33757  locfinref  34019  oms0  34475  bnj105  34901  ssoninhaus  36664  onint1  36665  bj-tagex  37235  bj-1uplex  37256  rrnval  38078  lsatset  39366  mnuprdlem2  44629  mnuprdlem3  44630  dvnprodlem3  46306  ioorrnopn  46663  ioorrnopnxr  46665  ismeannd  46825  nelsubc3  49430  setc1ohomfval  49852