Theorem p0ex 5083

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4561	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5014	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5080	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2903	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2166  Vcvv 3414  ∅c0 4144  𝒫 cpw 4378  {csn 4397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-dif 3801  df-in 3805  df-ss 3812  df-nul 4145  df-pw 4380  df-sn 4398

This theorem is referenced by:  pp0ex  5085  dtruALT  5087  zfpair  5125  opthprc  5400  snsn0non  6081  fvclex  7400  tposexg  7631  2dom  8295  endisj  8316  pw2eng  8335  dfac4  9258  dfac2b  9266  dfac2OLD  9268  cdaval  9307  axcc2lem  9573  axdc2lem  9585  axcclem  9594  axpowndlem3  9736  isstruct2  16232  plusffval  17600  staffval  19203  scaffval  19237  lpival  19606  ipffval  20355  refun0  21689  filconn  22057  alexsubALTlem2  22222  nmfval  22763  tcphex  23385  tchnmfval  23396  legval  25896  locfinref  30453  oms0  30904  bnj105  31339  ssoninhaus  32980  onint1  32981  bj-tagex  33497  bj-1uplex  33518  lindsadd  33946  rrnval  34168  lsatset  35065  dvnprodlem3  40958  ioorrnopn  41316  ioorrnopnxr  41318  ismeannd  41475