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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4017 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4419 . . 3  |-  (/)  e.  _V
32pwex 4472 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2512 1  |-  { (/) }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   _Vcvv 2970   (/)c0 3634   ~Pcpw 3857   {csn 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-in 3332  df-ss 3339  df-nul 3635  df-pw 3859  df-sn 3875
This theorem is referenced by:  pp0ex  4478  dtruALT  4521  zfpair  4526  snsn0non  4833  opthprc  4882  fvclex  6548  tposexg  6758  2dom  7378  map1  7384  endisj  7394  pw2eng  7413  dfac4  8288  dfac2  8296  cdaval  8335  axcc2lem  8601  axdc2lem  8613  axcclem  8622  axpowndlem3  8760  axpowndlem3OLD  8761  ccatfn  12268  isstruct2  14179  plusffval  15423  staffval  16912  scaffval  16946  lpival  17305  ipffval  18036  tgdif0  18556  filcon  19415  alexsubALTlem2  19579  nmfval  20140  tchex  20691  tchnmfval  20702  legval  22970  rankeq1o  28138  ssoninhaus  28224  onint1  28225  rrnval  28651  bnj105  31547  bj-tagex  32210  bj-1uplex  32231  lsatset  32357
  Copyright terms: Public domain W3C validator