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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4035 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4437 . . 3  |-  (/)  e.  _V
32pwex 4490 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2514 1  |-  { (/) }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2987   (/)c0 3652   ~Pcpw 3875   {csn 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pow 4485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-v 2989  df-dif 3346  df-in 3350  df-ss 3357  df-nul 3653  df-pw 3877  df-sn 3893
This theorem is referenced by:  pp0ex  4496  dtruALT  4539  zfpair  4544  snsn0non  4852  opthprc  4901  fvclex  6564  tposexg  6774  2dom  7397  map1  7403  endisj  7413  pw2eng  7432  dfac4  8307  dfac2  8315  cdaval  8354  axcc2lem  8620  axdc2lem  8632  axcclem  8641  axpowndlem3  8779  axpowndlem3OLD  8780  ccatfn  12287  isstruct2  14198  plusffval  15442  staffval  16947  scaffval  16981  lpival  17342  ipffval  18092  tgdif0  18612  filcon  19471  alexsubALTlem2  19635  nmfval  20196  tchex  20747  tchnmfval  20758  legval  23030  oms0  26725  rankeq1o  28224  ssoninhaus  28309  onint1  28310  rrnval  28745  bnj105  31732  bj-tagex  32499  bj-1uplex  32520  lsatset  32654
  Copyright terms: Public domain W3C validator