Theorem p0ex 4232

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

Assertion

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

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 3780	. 2 |- ~P (/) = { (/) }
2		0ex 4171	. . 3 |- (/) e. _V
3	2	pwex 4227	. 2 |- ~P (/) e. _V
4	1, 3	eqeltrri 2279	1 |- { (/) } e. _V

Syntax hints:   e. wcel 2176   _Vcvv 2772   (/)c0 3460   ~Pcpw 3616   {csn 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-nul 4170  ax-pow 4218

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639

This theorem is referenced by:  pp0ex  4233  undifexmid  4237  exmidexmid  4240  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  ordtriexmidlem  4567  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmid  4578  regexmidlemm  4580  ordsoexmid  4610  ordtri2or2exmid  4619  ontri2orexmidim  4620  opthprc  4726  acexmidlema  5935  acexmidlem2  5941  tposexg  6344  2dom  6897  map1  6904  endisj  6919  ssfiexmid  6973  domfiexmid  6975  exmidpw  7005  exmidpw2en  7009  djuex  7145  exmidomni  7244  exmidonfinlem  7301  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  pw1dom2  7339  pw1ne1  7341  sbthom  15965