Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  p0ex Structured version   Visualization version   GIF version

Theorem p0ex 5272
 Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5273. (Contributed by NM, 23-Dec-1993.)
Assertion
Ref Expression
p0ex {∅} ∈ V

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4729 . 2 𝒫 ∅ = {∅}
2 0ex 5197 . . 3 ∅ ∈ V
32pwex 5268 . 2 𝒫 ∅ ∈ V
41, 3eqeltrri 2913 1 {∅} ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2115  Vcvv 3480  ∅c0 4276  𝒫 cpw 4522  {csn 4550 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936  df-nul 4277  df-pw 4524  df-sn 4551 This theorem is referenced by:  pp0ex  5274  dtruALT  5276  zfpair  5309  tposexg  7902  endisj  8600  pw2eng  8619  dfac4  9546  dfac2b  9554  axcc2lem  9856  axdc2lem  9868  axcclem  9877  axpowndlem3  10019  isstruct2  16493  plusffval  17858  grpinvfval  18142  grpsubfval  18147  mulgfval  18226  0symgefmndeq  18522  staffval  19618  scaffval  19652  lpival  20018  ipffval  20792  refun0  22123  filconn  22491  alexsubALTlem2  22656  nmfval  23198  tcphex  23824  tchnmfval  23835  legval  26381  locfinref  31165  oms0  31612  bnj105  32051  ssoninhaus  33853  onint1  33854  bj-tagex  34367  bj-1uplex  34388  rrnval  35210  lsatset  36231  mnuprdlem2  40901  mnuprdlem3  40902  dvnprodlem3  42516  ioorrnopn  42873  ioorrnopnxr  42875  ismeannd  43032
 Copyright terms: Public domain W3C validator