HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-eu Unicode version
Definition df-eu 123
Description: Define the 'exists unique' operator.
Assertion
Ref Expression
df-eu |- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
Distinct variable group:   x,p,y
Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 kt 8 . 2 term T.
2 teu 115 . . 3 term E!
3 hal . . . . 5 type al
4 hb 3 . . . . 5 type *
53, 4ht 2 . . . 4 type (al -> *)
6 vp . . . 4 var p
7 tex 113 . . . . 5 term E.
8 vy . . . . . 6 var y
9 tal 112 . . . . . . 7 term A.
10 vx . . . . . . . 8 var x
115, 6tv 1 . . . . . . . . . 10 term p:(al -> *)
123, 10tv 1 . . . . . . . . . 10 term x:al
1311, 12kc 5 . . . . . . . . 9 term (p:(al -> *)x:al)
143, 8tv 1 . . . . . . . . . 10 term y:al
15 ke 7 . . . . . . . . . 10 term =
1612, 14, 15kbr 9 . . . . . . . . 9 term [x:al = y:al]
1713, 16, 15kbr 9 . . . . . . . 8 term [(p:(al -> *)x:al) = [x:al = y:al]]
183, 10, 17kl 6 . . . . . . 7 term \x:al [(p:(al -> *)x:al) = [x:al = y:al]]
199, 18kc 5 . . . . . 6 term (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])
203, 8, 19kl 6 . . . . 5 term \y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]])
217, 20kc 5 . . . 4 term (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))
225, 6, 21kl 6 . . 3 term \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))
232, 22, 15kbr 9 . 2 term [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
241, 23wffMMJ2 11 1 wff T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
Colors of variables: type var term
This definition is referenced by:  weu  131  euval  134
  Copyright terms: Public domain W3C validator