Theorem p0ex 5379

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

Syntax hints:   ∈ wcel 2099  Vcvv 3463  ∅c0 4323  𝒫 cpw 4598  {csn 4624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3465  df-dif 3950  df-ss 3964  df-nul 4324  df-pw 4600  df-sn 4625

This theorem is referenced by:  pp0ex  5381  dtruALT  5383  zfpair  5416  tposexg  8245  fsetexb  8883  endisj  9086  pw2eng  9106  dfac4  10156  dfac2b  10164  axcc2lem  10468  axdc2lem  10480  axcclem  10489  axpowndlem3  10631  isstruct2  17144  cat1  18112  plusffval  18632  grpinvfval  18966  grpsubfval  18971  mulgfval  19057  0symgefmndeq  19385  staffval  20814  scaffval  20850  lpival  21307  ipffval  21638  refun0  23505  filconn  23873  alexsubALTlem2  24038  nmfval  24583  tcphex  25231  tchnmfval  25242  legval  28506  locfinref  33667  oms0  34142  bnj105  34580  ssoninhaus  36171  onint1  36172  bj-tagex  36705  bj-1uplex  36726  rrnval  37539  lsatset  38699  mnuprdlem2  43982  mnuprdlem3  43983  dvnprodlem3  45603  ioorrnopn  45960  ioorrnopnxr  45962  ismeannd  46122