Theorem p0ex 5329

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  𝒫 cpw 4554  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918  df-nul 4286  df-pw 4556  df-sn 4581

This theorem is referenced by:  pp0ex  5331  dtruALT  5333  zfpair  5366  tposexg  8182  fsetexb  8801  endisj  8992  pw2eng  9011  dfac4  10032  dfac2b  10041  axcc2lem  10346  axdc2lem  10358  axcclem  10367  axpowndlem3  10510  isstruct2  17076  cat1  18021  plusffval  18571  grpinvfval  18908  grpsubfval  18913  mulgfval  18999  0symgefmndeq  19323  staffval  20774  scaffval  20831  lpival  21279  ipffval  21603  refun0  23459  filconn  23827  alexsubALTlem2  23992  nmfval  24532  tcphex  25173  tchnmfval  25184  legval  28656  vieta  33736  locfinref  33998  oms0  34454  bnj105  34880  ssoninhaus  36642  onint1  36643  bj-tagex  37188  bj-1uplex  37209  rrnval  38028  lsatset  39250  mnuprdlem2  44514  mnuprdlem3  44515  dvnprodlem3  46192  ioorrnopn  46549  ioorrnopnxr  46551  ismeannd  46711  nelsubc3  49316  setc1ohomfval  49738