Theorem leqf 169

Description: Equality theorem for lambda abstraction, using bound variable instead of distinct variables.

Hypotheses

Ref	Expression
leqf.1	|- A:be
leqf.2	|- R |= [A = B]
leqf.3	|- T. |= [(\x:al Ry:al) = R]

Assertion

Ref	Expression
leqf	|- R |= [\x:al A = \x:al B]

Distinct variable groups:   y,A   y,B   y,R   x,y,al

Proof of Theorem leqf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		leqf.1	. . . . 5 |- A:be
2	1	wl 59	. . . 4 |- \x:al A:(al -> be)
3		wv 58	. . . 4 |- z:al:al
4	2, 3	wc 45	. . 3 |- (\x:al Az:al):be
5	4	wl 59	. 2 |- \z:al (\x:al Az:al):(al -> be)
6		leqf.2	. . . . 5 |- R |= [A = B]
7	6	ax-cb1 29	. . . . . 6 |- R:*
8	1	beta 82	. . . . . 6 |- T. |= [(\x:al Ax:al) = A]
9	7, 8	a1i 28	. . . . 5 |- R |= [(\x:al Ax:al) = A]
10	1, 6	eqtypi 69	. . . . . . 7 |- B:be
11	10	beta 82	. . . . . 6 |- T. |= [(\x:al Bx:al) = B]
12	7, 11	a1i 28	. . . . 5 |- R |= [(\x:al Bx:al) = B]
13	1, 6, 9, 12	3eqtr4i 86	. . . 4 |- R |= [(\x:al Ax:al) = (\x:al Bx:al)]
14		weq 38	. . . . 5 |- = :(be -> (be -> *))
15		wv 58	. . . . 5 |- y:al:al
16	10	wl 59	. . . . . 6 |- \x:al B:(al -> be)
17	16, 3	wc 45	. . . . 5 |- (\x:al Bz:al):be
18	14, 15	ax-17 95	. . . . 5 |- T. |= [(\x:al = y:al) = = ]
19	1, 15	ax-hbl1 93	. . . . . 6 |- T. |= [(\x:al \x:al Ay:al) = \x:al A]
20	3, 15	ax-17 95	. . . . . 6 |- T. |= [(\x:al z:aly:al) = z:al]
21	2, 3, 15, 19, 20	hbc 100	. . . . 5 |- T. |= [(\x:al (\x:al Az:al)y:al) = (\x:al Az:al)]
22	10, 15	ax-hbl1 93	. . . . . 6 |- T. |= [(\x:al \x:al By:al) = \x:al B]
23	16, 3, 15, 22, 20	hbc 100	. . . . 5 |- T. |= [(\x:al (\x:al Bz:al)y:al) = (\x:al Bz:al)]
24	14, 4, 15, 17, 18, 21, 23	hbov 101	. . . 4 |- T. |= [(\x:al [(\x:al Az:al) = (\x:al Bz:al)]y:al) = [(\x:al Az:al) = (\x:al Bz:al)]]
25		leqf.3	. . . 4 |- T. |= [(\x:al Ry:al) = R]
26		wv 58	. . . . . 6 |- x:al:al
27	2, 26	wc 45	. . . . 5 |- (\x:al Ax:al):be
28	16, 26	wc 45	. . . . 5 |- (\x:al Bx:al):be
29	26, 3	weqi 68	. . . . . . 7 |- [x:al = z:al]:*
30	29	id 25	. . . . . 6 |- [x:al = z:al] |= [x:al = z:al]
31	2, 26, 30	ceq2 80	. . . . 5 |- [x:al = z:al] |= [(\x:al Ax:al) = (\x:al Az:al)]
32	16, 26, 30	ceq2 80	. . . . 5 |- [x:al = z:al] |= [(\x:al Bx:al) = (\x:al Bz:al)]
33	14, 27, 28, 31, 32	oveq12 90	. . . 4 |- [x:al = z:al] |= [[(\x:al Ax:al) = (\x:al Bx:al)] = [(\x:al Az:al) = (\x:al Bz:al)]]
34	29, 7	eqid 73	. . . 4 |- [x:al = z:al] |= [R = R]
35	13, 24, 25, 33, 34	ax-inst 103	. . 3 |- R |= [(\x:al Az:al) = (\x:al Bz:al)]
36	4, 35	leq 81	. 2 |- R |= [\z:al (\x:al Az:al) = \z:al (\x:al Bz:al)]
37	2	eta 166	. . 3 |- T. |= [\z:al (\x:al Az:al) = \x:al A]
38	7, 37	a1i 28	. 2 |- R |= [\z:al (\x:al Az:al) = \x:al A]
39	16	eta 166	. . 3 |- T. |= [\z:al (\x:al Bz:al) = \x:al B]
40	7, 39	a1i 28	. 2 |- R |= [\z:al (\x:al Bz:al) = \x:al B]
41	5, 36, 38, 40	3eqtr3i 87	1 |- R |= [\x:al A = \x:al B]

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-hbl1 93  ax-17 95  ax-inst 103  ax-eta 165

This theorem depends on definitions:  df-ov 65  df-al 116

This theorem is referenced by:  alrimi  170  axext  206  axrep  207