Theorem p0ex 2776

Description: The power set of the empty set is a set.

Assertion

Ref	Expression
p0ex	|- {(/)} e. V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		snex 2756	1 |- {(/)} e. V

Syntax hints:   e. wcel 960  Vcvv 1814  (/)c0 2283  {csn 2413

This theorem is referenced by:  pp0ex 2777  dtru 2778  zfpair 2783  snsn0non 3131  opthprc 3227  fvclex 3862  ensn1 4430  en1 4432  2dom 4433  map1 4436  endisj 4443  pw2en 4452  1sdom2 4531  unxpdom2 4856  sucxpdom 4857  cdavalt 4931  uncdadom 4933  cdaassen 4942  xpcdaen 4943  mapcdaen 4944  cdadom1 4945  axpowndlem3 4963  infxpidmlem9 7561  sn0top 7644

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416

Copyright terms: Public domain