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  18035  plusffval  18549  grpinvfval  18886  grpsubfval  18891  mulgfval  18977  0symgefmndeq  19300  staffval  20726  scaffval  20762  lpival  21210  ipffval  21533  refun0  23378  filconn  23746  alexsubALTlem2  23911  nmfval  24452  tcphex  25093  tchnmfval  25104  legval  28487  locfinref  33804  oms0  34261  bnj105  34687  ssoninhaus  36409  onint1  36410  bj-tagex  36948  bj-1uplex  36969  rrnval  37794  lsatset  38956  mnuprdlem2  44235  mnuprdlem3  44236  dvnprodlem3  45919  ioorrnopn  46276  ioorrnopnxr  46278  ismeannd  46438  nelsubc3  49033  setc1ohomfval  49455