Theorem p0ex 5349

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4773	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5264	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5345	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2857	1 ⊢ {∅} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  𝒫 cpw 4557  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916  df-nul 4280  df-pw 4559  df-sn 4585

This theorem is used by:  pp0ex  5351  dtruALT  5353  zfpair  5386  tposexg  8239  fsetexb  8866  endisj  9063  pw2eng  9082  dfac4  10126  dfac2b  10134  axcc2lem  10439  axdc2lem  10451  axcclem  10460  axpowndlem3  10609  isstruct2  17242  cat1  18187  plusffval  18737  grpinvfval  19103  grpsubfval  19108  mulgfval  19193  0symgefmndeq  19522  staffval  21008  scaffval  21065  ipffval  21862  refun0  23742  filconn  24110  alexsubALTlem2  24275  nmfval  24815  tcphex  25446  tchnmfval  25457  legval  28927  vieta  34091  locfinref  34352  oms0  34809  bnj105  35235  ssoninhaus  37068  onint1  37069  bj-tagex  37732  bj-1uplex  37753  rrnval  38578  dvnprodlem3  46777  ioorrnopn  47134  ioorrnopnxr  47136  ismeannd  47296  nelsubc3  49998  setc1ohomfval  50420