Theorem p0ex 5250

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4705	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5175	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5246	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2887	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ∅c0 4243  𝒫 cpw 4497  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526

This theorem is referenced by:  pp0ex  5252  dtruALT  5254  zfpair  5287  tposexg  7889  endisj  8587  pw2eng  8606  dfac4  9533  dfac2b  9541  axcc2lem  9847  axdc2lem  9859  axcclem  9868  axpowndlem3  10010  isstruct2  16485  plusffval  17850  grpinvfval  18134  grpsubfval  18139  mulgfval  18218  0symgefmndeq  18514  staffval  19611  scaffval  19645  lpival  20011  ipffval  20337  refun0  22120  filconn  22488  alexsubALTlem2  22653  nmfval  23195  tcphex  23821  tchnmfval  23832  legval  26378  locfinref  31194  oms0  31665  bnj105  32104  ssoninhaus  33909  onint1  33910  bj-tagex  34423  bj-1uplex  34444  rrnval  35265  lsatset  36286  mnuprdlem2  40981  mnuprdlem3  40982  dvnprodlem3  42590  ioorrnopn  42947  ioorrnopnxr  42949  ismeannd  43106