Theorem p0ex 5346

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4773	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5261	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5342	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2858	1 ⊢ {∅} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  𝒫 cpw 4557  {csn 4584

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916  df-nul 4280  df-pw 4559  df-sn 4585

This theorem is used by:  pp0ex  5348  dtruALT  5350  zfpair  5383  tposexg  8257  fsetexb  8886  endisj  9083  pw2eng  9102  dfac4  10201  dfac2b  10209  axcc2lem  10514  axdc2lem  10526  axcclem  10535  axpowndlem3  10684  isstruct2  17327  cat1  18272  plusffval  18822  grpinvfval  19189  grpsubfval  19194  mulgfval  19279  0symgefmndeq  19608  staffval  21098  scaffval  21155  ipffval  21954  refun0  23834  filconn  24202  alexsubALTlem2  24367  nmfval  24907  tcphex  25538  tchnmfval  25549  legval  29047  vieta  34212  locfinref  34473  oms0  34929  bnj105  35355  ssoninhaus  37236  onint1  37237  bj-tagex  37900  bj-1uplex  37921  rrnval  38761  dvnprodlem3  46957  ioorrnopn  47314  ioorrnopnxr  47316  ismeannd  47476  nelsubc3  50178  setc1ohomfval  50600