Theorem p0ex 5355

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4778	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5270	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5351	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2860	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  𝒫 cpw 4562  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922  df-nul 4287  df-pw 4564  df-sn 4590

This theorem is referenced by:  pp0ex  5357  dtruALT  5359  zfpair  5392  tposexg  8232  fsetexb  8857  endisj  9048  pw2eng  9067  dfac4  10102  dfac2b  10110  axcc2lem  10415  axdc2lem  10427  axcclem  10436  axpowndlem3  10579  isstruct2  17204  cat1  18149  plusffval  18699  grpinvfval  19040  grpsubfval  19045  mulgfval  19130  0symgefmndeq  19459  staffval  20944  scaffval  21001  ipffval  21798  refun0  23672  filconn  24040  alexsubALTlem2  24205  nmfval  24745  tcphex  25376  tchnmfval  25387  legval  28853  vieta  33970  locfinref  34231  oms0  34687  bnj105  35113  ssoninhaus  36959  onint1  36960  bj-tagex  37623  bj-1uplex  37644  rrnval  38478  dvnprodlem3  46662  ioorrnopn  47019  ioorrnopnxr  47021  ismeannd  47181  nelsubc3  49849  setc1ohomfval  50271