Theorem p0ex 5384

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4812	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5307	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5380	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2838	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  𝒫 cpw 4600  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334  df-pw 4602  df-sn 4627

This theorem is referenced by:  pp0ex  5386  dtruALT  5388  zfpair  5421  tposexg  8265  fsetexb  8904  endisj  9098  pw2eng  9118  dfac4  10162  dfac2b  10171  axcc2lem  10476  axdc2lem  10488  axcclem  10497  axpowndlem3  10639  isstruct2  17186  cat1  18142  plusffval  18659  grpinvfval  18996  grpsubfval  19001  mulgfval  19087  0symgefmndeq  19411  staffval  20842  scaffval  20878  lpival  21334  ipffval  21666  refun0  23523  filconn  23891  alexsubALTlem2  24056  nmfval  24601  tcphex  25251  tchnmfval  25262  legval  28592  locfinref  33840  oms0  34299  bnj105  34738  ssoninhaus  36449  onint1  36450  bj-tagex  36988  bj-1uplex  37009  rrnval  37834  lsatset  38991  mnuprdlem2  44292  mnuprdlem3  44293  dvnprodlem3  45963  ioorrnopn  46320  ioorrnopnxr  46322  ismeannd  46482