Theorem p0ex 5402

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

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4837	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 5325	. . 3 ⊢ ∅ ∈ V
3	2	pwex 5398	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2841	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  𝒫 cpw 4622  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993  df-nul 4353  df-pw 4624  df-sn 4649

This theorem is referenced by:  pp0ex  5404  dtruALT  5406  zfpair  5439  tposexg  8281  fsetexb  8922  endisj  9124  pw2eng  9144  dfac4  10191  dfac2b  10200  axcc2lem  10505  axdc2lem  10517  axcclem  10526  axpowndlem3  10668  isstruct2  17196  cat1  18164  plusffval  18684  grpinvfval  19018  grpsubfval  19023  mulgfval  19109  0symgefmndeq  19435  staffval  20864  scaffval  20900  lpival  21357  ipffval  21689  refun0  23544  filconn  23912  alexsubALTlem2  24077  nmfval  24622  tcphex  25270  tchnmfval  25281  legval  28610  locfinref  33787  oms0  34262  bnj105  34700  ssoninhaus  36414  onint1  36415  bj-tagex  36953  bj-1uplex  36974  rrnval  37787  lsatset  38946  mnuprdlem2  44242  mnuprdlem3  44243  dvnprodlem3  45869  ioorrnopn  46226  ioorrnopnxr  46228  ismeannd  46388