Definition df-eu 133

Description: Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-eu	⊢ ⊤⊧[∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]

Distinct variable group:   x,p,y

Detailed syntax breakdown of Definition df-eu

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		teu 125	. . 3 term ∃!
3		hal	. . . . 5 type α
4		hb 3	. . . . 5 type ∗
5	3, 4	ht 2	. . . 4 type (α → ∗)
6		vp	. . . 4 var p
7		tex 123	. . . . 5 term ∃
8		vy	. . . . . 6 var y
9		tal 122	. . . . . . 7 term ∀
10		vx	. . . . . . . 8 var x
11	5, 6	tv 1	. . . . . . . . . 10 term p:(α → ∗)
12	3, 10	tv 1	. . . . . . . . . 10 term x:α
13	11, 12	kc 5	. . . . . . . . 9 term (p:(α → ∗)x:α)
14	3, 8	tv 1	. . . . . . . . . 10 term y:α
15		ke 7	. . . . . . . . . 10 term =
16	12, 14, 15	kbr 9	. . . . . . . . 9 term [x:α = y:α]
17	13, 16, 15	kbr 9	. . . . . . . 8 term [(p:(α → ∗)x:α) = [x:α = y:α]]
18	3, 10, 17	kl 6	. . . . . . 7 term λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]
19	9, 18	kc 5	. . . . . 6 term (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])
20	3, 8, 19	kl 6	. . . . 5 term λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]])
21	7, 20	kc 5	. . . 4 term (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))
22	5, 6, 21	kl 6	. . 3 term λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))
23	2, 22, 15	kbr 9	. 2 term [∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
24	1, 23	wffMMJ2 11	1 wff ⊤⊧[∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]

This definition is referenced by:  weu  141  euval  144