Definition df-f11 194

Description: Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
df-f11	|- T. |= [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-f11

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tf11 189	. . 3 term 1-1
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		tal 122	. . . . 5 term A.
8		vx	. . . . . 6 var x
9		vy	. . . . . . . 8 var y
10	5, 6	tv 1	. . . . . . . . . . 11 term f:(al -> be)
11	3, 8	tv 1	. . . . . . . . . . 11 term x:al
12	10, 11	kc 5	. . . . . . . . . 10 term (f:(al -> be)x:al)
13	3, 9	tv 1	. . . . . . . . . . 11 term y:al
14	10, 13	kc 5	. . . . . . . . . 10 term (f:(al -> be)y:al)
15		ke 7	. . . . . . . . . 10 term =
16	12, 14, 15	kbr 9	. . . . . . . . 9 term [(f:(al -> be)x:al) = (f:(al -> be)y:al)]
17	11, 13, 15	kbr 9	. . . . . . . . 9 term [x:al = y:al]
18		tim 121	. . . . . . . . 9 term ==>
19	16, 17, 18	kbr 9	. . . . . . . 8 term [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]
20	3, 9, 19	kl 6	. . . . . . 7 term \y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]
21	7, 20	kc 5	. . . . . 6 term (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]])
22	3, 8, 21	kl 6	. . . . 5 term \x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]])
23	7, 22	kc 5	. . . 4 term (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))
24	5, 6, 23	kl 6	. . 3 term \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))
25	2, 24, 15	kbr 9	. 2 term [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]
26	1, 25	wffMMJ2 11	1 wff T. |= [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]

This definition is referenced by: (None)