Theorem p0ex 5322

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  𝒫 cpw 4542  {csn 4568

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 5232  ax-nul 5242  ax-pow 5303

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 3432  df-dif 3893  df-ss 3907  df-nul 4275  df-pw 4544  df-sn 4569

This theorem is referenced by:  pp0ex  5324  dtruALT  5326  zfpair  5359  tposexg  8184  fsetexb  8805  endisj  8996  pw2eng  9015  dfac4  10038  dfac2b  10047  axcc2lem  10352  axdc2lem  10364  axcclem  10373  axpowndlem3  10516  isstruct2  17113  cat1  18058  plusffval  18608  grpinvfval  18948  grpsubfval  18953  mulgfval  19039  0symgefmndeq  19363  staffval  20812  scaffval  20869  ipffval  21641  refun0  23493  filconn  23861  alexsubALTlem2  24026  nmfval  24566  tcphex  25197  tchnmfval  25208  legval  28669  vieta  33742  locfinref  34004  oms0  34460  bnj105  34886  ssoninhaus  36649  onint1  36650  bj-tagex  37313  bj-1uplex  37334  rrnval  38165  dvnprodlem3  46397  ioorrnopn  46754  ioorrnopnxr  46756  ismeannd  46916  nelsubc3  49561  setc1ohomfval  49983