Theorem p0ex 5323

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4763	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5246	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5319	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2825	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  𝒫 cpw 4551  {csn 4577

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304

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 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920  df-nul 4285  df-pw 4553  df-sn 4578

This theorem is referenced by:  pp0ex  5325  dtruALT  5327  zfpair  5360  tposexg  8173  fsetexb  8791  endisj  8981  pw2eng  9000  dfac4  10016  dfac2b  10025  axcc2lem  10330  axdc2lem  10342  axcclem  10351  axpowndlem3  10493  isstruct2  17060  cat1  18004  plusffval  18520  grpinvfval  18857  grpsubfval  18862  mulgfval  18948  0symgefmndeq  19273  staffval  20726  scaffval  20783  lpival  21231  ipffval  21555  refun0  23400  filconn  23768  alexsubALTlem2  23933  nmfval  24474  tcphex  25115  tchnmfval  25126  legval  28529  locfinref  33808  oms0  34265  bnj105  34691  ssoninhaus  36422  onint1  36423  bj-tagex  36961  bj-1uplex  36982  rrnval  37807  lsatset  38969  mnuprdlem2  44246  mnuprdlem3  44247  dvnprodlem3  45929  ioorrnopn  46286  ioorrnopnxr  46288  ismeannd  46448  nelsubc3  49056  setc1ohomfval  49478