Theorem p0ex 5357

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5358. (Contributed by NM, 23-Dec-1993.)

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4780	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5272	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5353	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2862	1 ⊢ {∅} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ∅c0 4286  𝒫 cpw 4564  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923  df-nul 4287  df-pw 4566  df-sn 4592

This theorem is used by:  pp0ex  5359  dtruALT  5361  zfpair  5394  tposexg  8242  fsetexb  8867  endisj  9059  pw2eng  9078  dfac4  10122  dfac2b  10130  axcc2lem  10435  axdc2lem  10447  axcclem  10456  axpowndlem3  10599  isstruct2  17231  cat1  18176  plusffval  18726  grpinvfval  19089  grpsubfval  19094  mulgfval  19179  0symgefmndeq  19508  staffval  20994  scaffval  21051  ipffval  21848  refun0  23723  filconn  24091  alexsubALTlem2  24256  nmfval  24796  tcphex  25427  tchnmfval  25438  legval  28904  vieta  34034  locfinref  34295  oms0  34752  bnj105  35178  ssoninhaus  37016  onint1  37017  bj-tagex  37680  bj-1uplex  37701  rrnval  38536  dvnprodlem3  46720  ioorrnopn  47077  ioorrnopnxr  47079  ismeannd  47239  nelsubc3  49906  setc1ohomfval  50328