Theorem p0ex 5326

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4755	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5322	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2833	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  𝒫 cpw 4541  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906  df-nul 4274  df-pw 4543  df-sn 4568

This theorem is referenced by:  pp0ex  5328  dtruALT  5330  zfpair  5363  tposexg  8190  fsetexb  8811  endisj  9002  pw2eng  9021  dfac4  10044  dfac2b  10053  axcc2lem  10358  axdc2lem  10370  axcclem  10379  axpowndlem3  10522  isstruct2  17119  cat1  18064  plusffval  18614  grpinvfval  18954  grpsubfval  18959  mulgfval  19045  0symgefmndeq  19369  staffval  20818  scaffval  20875  ipffval  21628  refun0  23480  filconn  23848  alexsubALTlem2  24013  nmfval  24553  tcphex  25184  tchnmfval  25195  legval  28652  vieta  33724  locfinref  33985  oms0  34441  bnj105  34867  ssoninhaus  36630  onint1  36631  bj-tagex  37294  bj-1uplex  37315  rrnval  38148  dvnprodlem3  46376  ioorrnopn  46733  ioorrnopnxr  46735  ismeannd  46895  nelsubc3  49546  setc1ohomfval  49968