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	⊢ ⊤⊧(∀λf:(α → β) [λx:α (f:(α → β)x:α) = f:(α → β)])

Distinct variable group:   x,f

Detailed syntax breakdown of Axiom ax-eta

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tal 122	. . 3 term ∀
3		hal	. . . . 5 type α
4		hbe	. . . . 5 type β
5	3, 4	ht 2	. . . 4 type (α → β)
6		vf	. . . 4 var f
7		vx	. . . . . 6 var x
8	5, 6	tv 1	. . . . . . 7 term f:(α → β)
9	3, 7	tv 1	. . . . . . 7 term x:α
10	8, 9	kc 5	. . . . . 6 term (f:(α → β)x:α)
11	3, 7, 10	kl 6	. . . . 5 term λx:α (f:(α → β)x:α)
12		ke 7	. . . . 5 term =
13	11, 8, 12	kbr 9	. . . 4 term [λx:α (f:(α → β)x:α) = f:(α → β)]
14	5, 6, 13	kl 6	. . 3 term λf:(α → β) [λx:α (f:(α → β)x:α) = f:(α → β)]
15	2, 14	kc 5	. 2 term (∀λf:(α → β) [λx:α (f:(α → β)x:α) = f:(α → β)])
16	1, 15	wffMMJ2 11	1 wff ⊤⊧(∀λf:(α → β) [λx:α (f:(α → β)x:α) = f:(α → β)])

This axiom is referenced by:  eta  178