Theorem p0ex 5331

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5332. (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 5255	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5327	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2835	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3442  ∅c0 4273  𝒫 cpw 4551  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-dif 3904  df-in 3908  df-ss 3918  df-nul 4274  df-pw 4553  df-sn 4578

This theorem is referenced by:  pp0ex  5333  dtruALT  5335  zfpair  5368  tposexg  8130  fsetexb  8727  endisj  8927  pw2eng  8947  dfac4  9983  dfac2b  9991  axcc2lem  10297  axdc2lem  10309  axcclem  10318  axpowndlem3  10460  isstruct2  16947  cat1  17909  plusffval  18429  grpinvfval  18714  grpsubfval  18719  mulgfval  18798  0symgefmndeq  19097  staffval  20212  scaffval  20246  lpival  20621  ipffval  20958  refun0  22771  filconn  23139  alexsubALTlem2  23304  nmfval  23849  tcphex  24486  tchnmfval  24497  legval  27233  locfinref  32087  oms0  32562  bnj105  33001  ssoninhaus  34774  onint1  34775  bj-tagex  35312  bj-1uplex  35333  rrnval  36141  lsatset  37308  mnuprdlem2  42264  mnuprdlem3  42265  dvnprodlem3  43877  ioorrnopn  44234  ioorrnopnxr  44236  ismeannd  44394