Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-eu Unicode version

Definition df-eu 133
 Description: Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-eu
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-eu
StepHypRef Expression
1 kt 8 . 2 term
2 teu 125 . . 3 term
3 hal . . . . 5 type
4 hb 3 . . . . 5 type
53, 4ht 2 . . . 4 type
6 vp . . . 4 var
7 tex 123 . . . . 5 term
8 vy . . . . . 6 var
9 tal 122 . . . . . . 7 term
10 vx . . . . . . . 8 var
115, 6tv 1 . . . . . . . . . 10 term
123, 10tv 1 . . . . . . . . . 10 term
1311, 12kc 5 . . . . . . . . 9 term
143, 8tv 1 . . . . . . . . . 10 term
15 ke 7 . . . . . . . . . 10 term
1612, 14, 15kbr 9 . . . . . . . . 9 term
1713, 16, 15kbr 9 . . . . . . . 8 term
183, 10, 17kl 6 . . . . . . 7 term
199, 18kc 5 . . . . . 6 term
203, 8, 19kl 6 . . . . 5 term
217, 20kc 5 . . . 4 term
225, 6, 21kl 6 . . 3 term
232, 22, 15kbr 9 . 2 term
241, 23wffMMJ2 11 1 wff
 Colors of variables: type var term This definition is referenced by:  weu  141  euval  144
 Copyright terms: Public domain W3C validator