Theorem p0ex 2826

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 2806	1 |- {(/)} e. V

Syntax hints:   e. wcel 999  Vcvv 1858  (/)c0 2331  {csn 2461

This theorem is referenced by:  pp0ex 2827  dtru 2828  zfpair 2833  snsn0non 3182  opthprc 3278  fvclex 3913  ensn1 4485  en1 4487  2dom 4488  map1 4491  endisj 4500  pw2en 4509  1sdom2 4590  unxpdom2 4910  sucxpdom 4911  cdaval 4984  uncdadom 4986  cdaassen 4995  xpcdaen 4996  mapcdaen 4997  cdadom1 4998  axpowndlem3 5016  infxpidmlem9 7652  sn0top 7734

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464

Copyright terms: Public domain