Theorem p0ex 4186

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 3739	. 2 |- ~P (/) = { (/) }
2		0ex 4128	. . 3 |- (/) e. _V
3	2	pwex 4181	. 2 |- ~P (/) e. _V
4	1, 3	eqeltrri 2251	1 |- { (/) } e. _V

Syntax hints:   e. wcel 2148   _Vcvv 2737   (/)c0 3422   ~Pcpw 3575   {csn 3592

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-nul 4127  ax-pow 4172

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-dif 3131  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598

This theorem is referenced by:  pp0ex  4187  undifexmid  4191  exmidexmid  4194  exmidundif  4204  exmidundifim  4205  exmid1stab  4206  ordtriexmidlem  4516  ontr2exmid  4522  onsucsssucexmid  4524  onsucelsucexmid  4527  regexmidlemm  4529  ordsoexmid  4559  ordtri2or2exmid  4568  ontri2orexmidim  4569  opthprc  4675  acexmidlema  5861  acexmidlem2  5867  tposexg  6254  2dom  6800  map1  6807  endisj  6819  ssfiexmid  6871  domfiexmid  6873  exmidpw  6903  djuex  7037  exmidomni  7135  exmidonfinlem  7187  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  pw1dom2  7221  pw1ne1  7223  sbthom  14545