Theorem p0ex 5341

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4770	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5257	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5337	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2859	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ∅c0 4285  𝒫 cpw 4555  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921  df-nul 4286  df-pw 4557  df-sn 4583

This theorem is referenced by:  pp0ex  5343  dtruALT  5345  zfpair  5378  tposexg  8220  fsetexb  8845  endisj  9036  pw2eng  9055  dfac4  10078  dfac2b  10087  axcc2lem  10393  axdc2lem  10405  axcclem  10414  axpowndlem3  10557  isstruct2  17185  cat1  18130  plusffval  18680  grpinvfval  19020  grpsubfval  19025  mulgfval  19111  0symgefmndeq  19434  staffval  20890  scaffval  20947  ipffval  21700  refun0  23575  filconn  23943  alexsubALTlem2  24108  nmfval  24648  tcphex  25279  tchnmfval  25290  legval  28753  vieta  33877  locfinref  34138  oms0  34594  bnj105  35020  ssoninhaus  36808  onint1  36809  bj-tagex  37472  bj-1uplex  37493  rrnval  38326  dvnprodlem3  46522  ioorrnopn  46879  ioorrnopnxr  46881  ismeannd  47041  nelsubc3  49692  setc1ohomfval  50114