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

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

Proof of Theorem p0ex
StepHypRef Expression
1 pw0 4375 . 2 𝒫 ∅ = {∅}
2 0ex 4823 . . 3 ∅ ∈ V
32pwex 4878 . 2 𝒫 ∅ ∈ V
41, 3eqeltrri 2727 1 {∅} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  c0 3948  𝒫 cpw 4191  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949  df-pw 4193  df-sn 4211
This theorem is referenced by:  pp0ex  4885  dtruALT  4929  zfpair  4934  opthprc  5201  snsn0non  5884  fvclex  7180  tposexg  7411  2dom  8070  map1  8077  endisj  8088  pw2eng  8107  dfac4  8983  dfac2  8991  cdaval  9030  axcc2lem  9296  axdc2lem  9308  axcclem  9317  axpowndlem3  9459  isstruct2  15914  plusffval  17294  staffval  18895  scaffval  18929  lpival  19293  ipffval  20041  refun0  21366  filconn  21734  alexsubALTlem2  21899  nmfval  22440  tchex  23062  tchnmfval  23073  legval  25524  locfinref  30036  oms0  30487  bnj105  30918  rankeq1o  32403  ssoninhaus  32572  onint1  32573  bj-tagex  33100  bj-1uplex  33121  rrnval  33756  lsatset  34595  dvnprodlem3  40481  ioorrnopn  40843  ioorrnopnxr  40845  ismeannd  41002
  Copyright terms: Public domain W3C validator