Theorem p0ex 5342

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4779	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5265	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5338	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2826	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  𝒫 cpw 4566  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934  df-nul 4300  df-pw 4568  df-sn 4593

This theorem is referenced by:  pp0ex  5344  dtruALT  5346  zfpair  5379  tposexg  8222  fsetexb  8840  endisj  9032  pw2eng  9052  dfac4  10082  dfac2b  10091  axcc2lem  10396  axdc2lem  10408  axcclem  10417  axpowndlem3  10559  isstruct2  17126  cat1  18066  plusffval  18580  grpinvfval  18917  grpsubfval  18922  mulgfval  19008  0symgefmndeq  19331  staffval  20757  scaffval  20793  lpival  21241  ipffval  21564  refun0  23409  filconn  23777  alexsubALTlem2  23942  nmfval  24483  tcphex  25124  tchnmfval  25135  legval  28518  locfinref  33838  oms0  34295  bnj105  34721  ssoninhaus  36443  onint1  36444  bj-tagex  36982  bj-1uplex  37003  rrnval  37828  lsatset  38990  mnuprdlem2  44269  mnuprdlem3  44270  dvnprodlem3  45953  ioorrnopn  46310  ioorrnopnxr  46312  ismeannd  46472  nelsubc3  49064  setc1ohomfval  49486