Theorem p0ex 5339

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4776	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5262	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5335	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2825	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  𝒫 cpw 4563  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931  df-nul 4297  df-pw 4565  df-sn 4590

This theorem is referenced by:  pp0ex  5341  dtruALT  5343  zfpair  5376  tposexg  8219  fsetexb  8837  endisj  9028  pw2eng  9047  dfac4  10075  dfac2b  10084  axcc2lem  10389  axdc2lem  10401  axcclem  10410  axpowndlem3  10552  isstruct2  17119  cat1  18059  plusffval  18573  grpinvfval  18910  grpsubfval  18915  mulgfval  19001  0symgefmndeq  19324  staffval  20750  scaffval  20786  lpival  21234  ipffval  21557  refun0  23402  filconn  23770  alexsubALTlem2  23935  nmfval  24476  tcphex  25117  tchnmfval  25128  legval  28511  locfinref  33831  oms0  34288  bnj105  34714  ssoninhaus  36436  onint1  36437  bj-tagex  36975  bj-1uplex  36996  rrnval  37821  lsatset  38983  mnuprdlem2  44262  mnuprdlem3  44263  dvnprodlem3  45946  ioorrnopn  46303  ioorrnopnxr  46305  ismeannd  46465  nelsubc3  49060  setc1ohomfval  49482