Axiom ax-eta 177

Description: The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
ax-eta	|- T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])

Distinct variable group:   x,f

Detailed syntax breakdown of Axiom ax-eta

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tal 122	. . 3 term A.
3		hal	. . . . 5 type al
4		hbe	. . . . 5 type be
5	3, 4	ht 2	. . . 4 type (al -> be)
6		vf	. . . 4 var f
7		vx	. . . . . 6 var x
8	5, 6	tv 1	. . . . . . 7 term f:(al -> be)
9	3, 7	tv 1	. . . . . . 7 term x:al
10	8, 9	kc 5	. . . . . 6 term (f:(al -> be)x:al)
11	3, 7, 10	kl 6	. . . . 5 term \x:al (f:(al -> be)x:al)
12		ke 7	. . . . 5 term =
13	11, 8, 12	kbr 9	. . . 4 term [\x:al (f:(al -> be)x:al) = f:(al -> be)]
14	5, 6, 13	kl 6	. . 3 term \f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)]
15	2, 14	kc 5	. 2 term (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])
16	1, 15	wffMMJ2 11	1 wff T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])

This axiom is referenced by:  eta  178