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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4179 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4587 . . 3  |-  (/)  e.  _V
32pwex 4639 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2542 1  |-  { (/) }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819   _Vcvv 3109   (/)c0 3793   ~Pcpw 4015   {csn 4032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794  df-pw 4017  df-sn 4033
This theorem is referenced by:  pp0ex  4645  dtruALT  4688  zfpair  4693  snsn0non  5005  opthprc  5056  fvclex  6771  tposexg  6987  2dom  7607  map1  7613  endisj  7623  pw2eng  7642  dfac4  8520  dfac2  8528  cdaval  8567  axcc2lem  8833  axdc2lem  8845  axcclem  8854  axpowndlem3  8992  axpowndlem3OLD  8993  ccatfnOLD  12599  isstruct2  14652  plusffval  16003  staffval  17622  scaffval  17656  lpival  18019  ipffval  18809  refun0  20141  filcon  20509  alexsubALTlem2  20673  nmfval  21234  tchex  21785  tchnmfval  21796  legval  24096  locfinref  27997  oms0  28429  rankeq1o  29990  ssoninhaus  30075  onint1  30076  rrnval  30485  dvnprodlem3  31906  bnj105  33878  bj-tagex  34646  bj-1uplex  34667  lsatset  34816
  Copyright terms: Public domain W3C validator