Theorem p0ex 5334

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∅c0 4292  𝒫 cpw 4559  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928  df-nul 4293  df-pw 4561  df-sn 4586

This theorem is referenced by:  pp0ex  5336  dtruALT  5338  zfpair  5371  tposexg  8196  fsetexb  8814  endisj  9005  pw2eng  9024  dfac4  10051  dfac2b  10060  axcc2lem  10365  axdc2lem  10377  axcclem  10386  axpowndlem3  10528  isstruct2  17095  cat1  18039  plusffval  18555  grpinvfval  18892  grpsubfval  18897  mulgfval  18983  0symgefmndeq  19308  staffval  20761  scaffval  20818  lpival  21266  ipffval  21590  refun0  23435  filconn  23803  alexsubALTlem2  23968  nmfval  24509  tcphex  25150  tchnmfval  25161  legval  28564  locfinref  33824  oms0  34281  bnj105  34707  ssoninhaus  36429  onint1  36430  bj-tagex  36968  bj-1uplex  36989  rrnval  37814  lsatset  38976  mnuprdlem2  44255  mnuprdlem3  44256  dvnprodlem3  45939  ioorrnopn  46296  ioorrnopnxr  46298  ismeannd  46458  nelsubc3  49053  setc1ohomfval  49475