Theorem p0ex 4853

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

Assertion

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

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 4343	. 2 |- ~P (/) = { (/) }
2		0ex 4790	. . 3 |- (/) e. _V
3	2	pwex 4848	. 2 |- ~P (/) e. _V
4	1, 3	eqeltrri 2698	1 |- { (/) } e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   (/)c0 3915   ~Pcpw 4158   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178

This theorem is referenced by:  pp0ex  4855  dtruALT  4899  zfpair  4904  opthprc  5167  snsn0non  5846  fvclex  7138  tposexg  7366  2dom  8029  map1  8036  endisj  8047  pw2eng  8066  dfac4  8945  dfac2  8953  cdaval  8992  axcc2lem  9258  axdc2lem  9270  axcclem  9279  axpowndlem3  9421  isstruct2  15867  plusffval  17247  staffval  18847  scaffval  18881  lpival  19245  ipffval  19993  refun0  21318  filconn  21687  alexsubALTlem2  21852  nmfval  22393  tchex  23016  tchnmfval  23027  legval  25479  locfinref  29908  oms0  30359  bnj105  30790  rankeq1o  32278  ssoninhaus  32447  onint1  32448  bj-tagex  32975  bj-1uplex  32996  rrnval  33626  lsatset  34277  dvnprodlem3  40163  ioorrnopn  40525  ioorrnopnxr  40527  ismeannd  40684