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

Theorem p0ex 4818
 Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 4819. (Contributed by NM, 23-Dec-1993.)
Assertion
Ref Expression
p0ex {∅} ∈ V

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4316 . 2 𝒫 ∅ = {∅}
2 0ex 4755 . . 3 ∅ ∈ V
32pwex 4813 . 2 𝒫 ∅ ∈ V
41, 3eqeltrri 2701 1 {∅} ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1992  Vcvv 3191  ∅c0 3896  𝒫 cpw 4135  {csn 4153 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3897  df-pw 4137  df-sn 4154 This theorem is referenced by:  pp0ex  4820  dtruALT  4865  zfpair  4870  opthprc  5132  snsn0non  5808  fvclex  7088  tposexg  7312  2dom  7974  map1  7981  endisj  7992  pw2eng  8011  dfac4  8890  dfac2  8898  cdaval  8937  axcc2lem  9203  axdc2lem  9215  axcclem  9224  axpowndlem3  9366  isstruct2  15785  plusffval  17163  staffval  18763  scaffval  18797  lpival  19159  ipffval  19907  refun0  21223  filconn  21592  alexsubALTlem2  21757  nmfval  22298  tchex  22919  tchnmfval  22930  legval  25374  locfinref  29682  oms0  30132  bnj105  30490  rankeq1o  31893  ssoninhaus  32062  onint1  32063  bj-tagex  32595  bj-1uplex  32616  rrnval  33225  lsatset  33724  dvnprodlem3  39437  ioorrnopn  39800  ioorrnopnxr  39802  ismeannd  39959
 Copyright terms: Public domain W3C validator