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

Theorem p0ex 4213
Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 4214. (Contributed by NM, 23-Dec-1993.)
Assertion
Ref Expression
p0ex  |-  { (/) }  e.  _V

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 3778 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4166 . . 3  |-  (/)  e.  _V
32pwex 4209 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2367 1  |-  { (/) }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   (/)c0 3468   ~Pcpw 3638   {csn 3653
This theorem is referenced by:  pp0ex  4215  dtruALT  4223  zfpair  4228  snsn0non  4527  opthprc  4752  fvclex  5777  2dom  6949  map1  6955  endisj  6965  pw2eng  6984  dfac4  7765  dfac2  7773  cdaval  7812  axcc2lem  8078  axdc2lem  8090  axcclem  8099  axpowndlem3  8237  ccatfn  11443  isstruct2  13173  plusffval  14395  staffval  15628  scaffval  15661  lpival  16013  ipffval  16568  tgdif0  16746  filcon  17594  alexsubALTlem2  17758  nmfval  18127  tchex  18665  tchnmfval  18675  rankeq1o  24873  ssoninhaus  24959  onint1  24960  rrnval  26654  bnj105  29066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469  df-pw 3640  df-sn 3659
  Copyright terms: Public domain W3C validator