Theorem p0ex 5389

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4816	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5312	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5385	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2835	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  𝒫 cpw 4604  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979  df-nul 4339  df-pw 4606  df-sn 4631

This theorem is referenced by:  pp0ex  5391  dtruALT  5393  zfpair  5426  tposexg  8263  fsetexb  8902  endisj  9096  pw2eng  9116  dfac4  10159  dfac2b  10168  axcc2lem  10473  axdc2lem  10485  axcclem  10494  axpowndlem3  10636  isstruct2  17182  cat1  18150  plusffval  18671  grpinvfval  19008  grpsubfval  19013  mulgfval  19099  0symgefmndeq  19425  staffval  20858  scaffval  20894  lpival  21351  ipffval  21683  refun0  23538  filconn  23906  alexsubALTlem2  24071  nmfval  24616  tcphex  25264  tchnmfval  25275  legval  28606  locfinref  33801  oms0  34278  bnj105  34716  ssoninhaus  36430  onint1  36431  bj-tagex  36969  bj-1uplex  36990  rrnval  37813  lsatset  38971  mnuprdlem2  44268  mnuprdlem3  44269  dvnprodlem3  45903  ioorrnopn  46260  ioorrnopnxr  46262  ismeannd  46422