Theorem p0ex 5319

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5320. (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 5242	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5315	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2825	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3433  ∅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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300

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 3435  df-dif 3902  df-ss 3916  df-nul 4281  df-pw 4549  df-sn 4574

This theorem is referenced by:  pp0ex  5321  dtruALT  5323  zfpair  5356  tposexg  8164  fsetexb  8782  endisj  8971  pw2eng  8990  dfac4  10004  dfac2b  10013  axcc2lem  10318  axdc2lem  10330  axcclem  10339  axpowndlem3  10481  isstruct2  17047  cat1  17991  plusffval  18507  grpinvfval  18844  grpsubfval  18849  mulgfval  18935  0symgefmndeq  19260  staffval  20710  scaffval  20767  lpival  21215  ipffval  21539  refun0  23384  filconn  23752  alexsubALTlem2  23917  nmfval  24457  tcphex  25098  tchnmfval  25109  legval  28516  locfinref  33822  oms0  34278  bnj105  34704  ssoninhaus  36439  onint1  36440  bj-tagex  36978  bj-1uplex  36999  rrnval  37824  lsatset  38986  mnuprdlem2  44263  mnuprdlem3  44264  dvnprodlem3  45943  ioorrnopn  46300  ioorrnopnxr  46302  ismeannd  46462  nelsubc3  49070  setc1ohomfval  49492