Theorem weu 141

Description: There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
weu	|- E!:((al -> *) -> *)

Proof of Theorem weu

Dummy variables p x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wex 139	. . . 4 |- E.:((al -> *) -> *)
2		wal 134	. . . . . 6 |- A.:((al -> *) -> *)
3		wv 64	. . . . . . . . 9 |- p:(al -> *):(al -> *)
4		wv 64	. . . . . . . . 9 |- x:al:al
5	3, 4	wc 50	. . . . . . . 8 |- (p:(al -> *)x:al):*
6		wv 64	. . . . . . . . 9 |- y:al:al
7	4, 6	weqi 76	. . . . . . . 8 |- [x:al = y:al]:*
8	5, 7	weqi 76	. . . . . . 7 |- [(p:(al -> *)x:al) = [x:al = y:al]]:*
9	8	wl 66	. . . . . 6 |- \x:al [(p:(al -> *)x:al) = [x:al = y:al]]:(al -> *)
10	2, 9	wc 50	. . . . 5 |- (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]):*
11	10	wl 66	. . . 4 |- \y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]):(al -> *)
12	1, 11	wc 50	. . 3 |- (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])):*
13	12	wl 66	. 2 |- \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])):((al -> *) -> *)
14		df-eu 133	. 2 |- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
15	13, 14	eqtypri 81	1 |- E!:((al -> *) -> *)

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  wffMMJ2t 12  A.tal 122  E.tex 123  E!teu 125

This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42  ax-wc 49  ax-wv 63  ax-wl 65  ax-wov 71  ax-eqtypri 80

This theorem depends on definitions:  df-al 126  df-an 128  df-im 129  df-ex 131  df-eu 133

This theorem is referenced by:  euval  144