HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  weu Unicode version
Theorem weu 131
Description: There exists unique type.
Assertion
Ref Expression
weu |- E!:((al -> *) -> *)
Proof of Theorem weu
Dummy variables p x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wex 129 . . . 4 |- E.:((al -> *) -> *)
2 wal 124 . . . . . 6 |- A.:((al -> *) -> *)
3 wv 58 . . . . . . . . 9 |- p:(al -> *):(al -> *)
4 wv 58 . . . . . . . . 9 |- x:al:al
53, 4wc 45 . . . . . . . 8 |- (p:(al -> *)x:al):*
6 wv 58 . . . . . . . . 9 |- y:al:al
74, 6weqi 68 . . . . . . . 8 |- [x:al = y:al]:*
85, 7weqi 68 . . . . . . 7 |- [(p:(al -> *)x:al) = [x:al = y:al]]:*
98wl 59 . . . . . 6 |- \x:al [(p:(al -> *)x:al) = [x:al = y:al]]:(al -> *)
102, 9wc 45 . . . . 5 |- (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]):*
1110wl 59 . . . 4 |- \y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]):(al -> *)
121, 11wc 45 . . 3 |- (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])):*
1312wl 59 . 2 |- \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])):((al -> *) -> *)
14 df-eu 123 . 2 |- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
1513, 14eqtypri 71 1 |- E!:((al -> *) -> *)
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  wffMMJ2t 12  A.tal 112  E.tex 113  E!teu 115
This theorem was proved from axioms:  ax-cb1 29  ax-refl 39
This theorem depends on definitions:  df-al 116  df-an 118  df-im 119  df-ex 121  df-eu 123
This theorem is referenced by:  euval  134
  Copyright terms: Public domain W3C validator