ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  p0ex Unicode version

Theorem p0ex 4185
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
StepHypRef Expression
1 pw0 3738 . 2  |-  ~P (/)  =  { (/)
}
2 0ex 4127 . . 3  |-  (/)  e.  _V
32pwex 4180 . 2  |-  ~P (/)  e.  _V
41, 3eqeltrri 2251 1  |-  { (/) }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2148   _Vcvv 2737   (/)c0 3422   ~Pcpw 3574   {csn 3591
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 4118  ax-nul 4126  ax-pow 4171
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 3576  df-sn 3597
This theorem is referenced by:  pp0ex  4186  undifexmid  4190  exmidexmid  4193  exmidundif  4203  exmidundifim  4204  exmid1stab  4205  ordtriexmidlem  4515  ontr2exmid  4521  onsucsssucexmid  4523  onsucelsucexmid  4526  regexmidlemm  4528  ordsoexmid  4558  ordtri2or2exmid  4567  ontri2orexmidim  4568  opthprc  4674  acexmidlema  5860  acexmidlem2  5866  tposexg  6253  2dom  6799  map1  6806  endisj  6818  ssfiexmid  6870  domfiexmid  6872  exmidpw  6902  djuex  7036  exmidomni  7134  exmidonfinlem  7186  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  exmidaclem  7201  pw1dom2  7220  pw1ne1  7222  sbthom  14430
  Copyright terms: Public domain W3C validator