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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4737 . 2 𝒫 ∅ = {∅}
2 0ex 5202 . . 3 ∅ ∈ V
32pwex 5272 . 2 𝒫 ∅ ∈ V
41, 3eqeltrri 2907 1 {∅} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3492  c0 4288  𝒫 cpw 4535  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289  df-pw 4537  df-sn 4558
This theorem is referenced by:  pp0ex  5277  dtruALT  5279  zfpair  5312  tposexg  7895  endisj  8592  pw2eng  8611  dfac4  9536  dfac2b  9544  axcc2lem  9846  axdc2lem  9858  axcclem  9867  axpowndlem3  10009  isstruct2  16481  plusffval  17846  grpinvfval  18080  grpsubfval  18085  mulgfval  18164  staffval  19547  scaffval  19581  lpival  19946  ipffval  20720  refun0  22051  filconn  22419  alexsubALTlem2  22584  nmfval  23125  tcphex  23747  tchnmfval  23758  legval  26297  locfinref  31004  oms0  31454  bnj105  31893  ssoninhaus  33693  onint1  33694  bj-tagex  34196  bj-1uplex  34217  rrnval  34986  lsatset  36006  mnuprdlem2  40486  mnuprdlem3  40487  dvnprodlem3  42109  ioorrnopn  42467  ioorrnopnxr  42469  ismeannd  42626
  Copyright terms: Public domain W3C validator