Theorem p0ex 5383

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4816	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5308	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5379	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2831	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ∅c0 4323  𝒫 cpw 4603  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324  df-pw 4605  df-sn 4630

This theorem is referenced by:  pp0ex  5385  dtruALT  5387  zfpair  5420  tposexg  8225  fsetexb  8858  endisj  9058  pw2eng  9078  dfac4  10117  dfac2b  10125  axcc2lem  10431  axdc2lem  10443  axcclem  10452  axpowndlem3  10594  isstruct2  17082  cat1  18047  plusffval  18567  grpinvfval  18863  grpsubfval  18868  mulgfval  18952  0symgefmndeq  19261  staffval  20455  scaffval  20490  lpival  20883  ipffval  21201  refun0  23019  filconn  23387  alexsubALTlem2  23552  nmfval  24097  tcphex  24734  tchnmfval  24745  legval  27835  locfinref  32821  oms0  33296  bnj105  33735  ssoninhaus  35333  onint1  35334  bj-tagex  35868  bj-1uplex  35889  rrnval  36695  lsatset  37860  mnuprdlem2  43032  mnuprdlem3  43033  dvnprodlem3  44664  ioorrnopn  45021  ioorrnopnxr  45023  ismeannd  45183