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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 3913 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4307 . . 3  |-  (/)  e.  _V
32pwex 4350 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2483 1  |-  { (/) }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2924   (/)c0 3596   ~Pcpw 3767   {csn 3782
This theorem is referenced by:  pp0ex  4356  dtruALT  4364  zfpair  4369  snsn0non  4667  opthprc  4892  fvclex  5948  tposexg  6460  2dom  7146  map1  7152  endisj  7162  pw2eng  7181  dfac4  7967  dfac2  7975  cdaval  8014  axcc2lem  8280  axdc2lem  8292  axcclem  8301  axpowndlem3  8438  ccatfn  11704  isstruct2  13441  plusffval  14665  staffval  15898  scaffval  15931  lpival  16279  ipffval  16842  tgdif0  17020  filcon  17876  alexsubALTlem2  18040  nmfval  18597  tchex  19137  tchnmfval  19147  rankeq1o  26024  ssoninhaus  26110  onint1  26111  rrnval  26434  bnj105  28807  lsatset  29485
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-v 2926  df-dif 3291  df-in 3295  df-ss 3302  df-nul 3597  df-pw 3769  df-sn 3788
  Copyright terms: Public domain W3C validator