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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 3974 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4370 . . 3  |-  (/)  e.  _V
32pwex 4417 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2514 1  |-  { (/) }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1728   _Vcvv 2965   (/)c0 3616   ~Pcpw 3828   {csn 3843
This theorem is referenced by:  pp0ex  4423  dtruALT  4431  zfpair  4436  snsn0non  4735  opthprc  4960  fvclex  6017  tposexg  6529  2dom  7215  map1  7221  endisj  7231  pw2eng  7250  dfac4  8041  dfac2  8049  cdaval  8088  axcc2lem  8354  axdc2lem  8366  axcclem  8375  axpowndlem3  8512  ccatfn  11779  isstruct2  13516  plusffval  14740  staffval  15973  scaffval  16006  lpival  16354  ipffval  16917  tgdif0  17095  filcon  17953  alexsubALTlem2  18117  nmfval  18674  tchex  19214  tchnmfval  19224  rankeq1o  26147  ssoninhaus  26233  onint1  26234  rrnval  26578  bnj105  29263  lsatset  29962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2967  df-dif 3312  df-in 3316  df-ss 3323  df-nul 3617  df-pw 3830  df-sn 3849
  Copyright terms: Public domain W3C validator