Theorem p0ex 4779

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4283	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 4718	. . 3 ⊢ ∅ ∈ V
3	2	pwex 4774	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2685	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ∅c0 3874  𝒫 cpw 4108  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-sn 4126

This theorem is referenced by:  pp0ex  4781  dtruALT  4826  zfpair  4831  opthprc  5089  snsn0non  5763  fvclex  7031  tposexg  7253  2dom  7915  map1  7921  endisj  7932  pw2eng  7951  dfac4  8828  dfac2  8836  cdaval  8875  axcc2lem  9141  axdc2lem  9153  axcclem  9162  axpowndlem3  9300  isstruct2  15704  plusffval  17070  staffval  18670  scaffval  18704  lpival  19066  ipffval  19812  refun0  21128  filcon  21497  alexsubALTlem2  21662  nmfval  22203  tchex  22824  tchnmfval  22835  legval  25279  locfinref  29236  oms0  29686  bnj105  30044  rankeq1o  31448  ssoninhaus  31617  onint1  31618  bj-tagex  32168  bj-1uplex  32189  rrnval  32796  lsatset  33295  dvnprodlem3  38838  ioorrnopn  39201  ioorrnopnxr  39203  ismeannd  39360