Theorem leqf 181

Description: Equality theorem for lambda abstraction, using bound variable instead of distinct variables. (Contributed by Mario Carneiro, 8-Oct-2014.)

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 66	. . . 4 |- \x:al A:(al -> be)
3		wv 64	. . . 4 |- z:al:al
4	2, 3	wc 50	. . 3 |- (\x:al Az:al):be
5	4	wl 66	. 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 92	. . . . . 6 |- T. |= [(\x:al Ax:al) = A]
9	7, 8	a1i 28	. . . . 5 |- R |= [(\x:al Ax:al) = A]
10	1, 6	eqtypi 78	. . . . . . 7 |- B:be
11	10	beta 92	. . . . . 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 96	. . . 4 |- R |= [(\x:al Ax:al) = (\x:al Bx:al)]
14		weq 41	. . . . 5 |- = :(be -> (be -> *))
15		wv 64	. . . . 5 |- y:al:al
16	10	wl 66	. . . . . 6 |- \x:al B:(al -> be)
17	16, 3	wc 50	. . . . 5 |- (\x:al Bz:al):be
18	14, 15	ax-17 105	. . . . 5 |- T. |= [(\x:al = y:al) = = ]
19	1, 15	ax-hbl1 103	. . . . . 6 |- T. |= [(\x:al \x:al Ay:al) = \x:al A]
20	3, 15	ax-17 105	. . . . . 6 |- T. |= [(\x:al z:aly:al) = z:al]
21	2, 3, 15, 19, 20	hbc 110	. . . . 5 |- T. |= [(\x:al (\x:al Az:al)y:al) = (\x:al Az:al)]
22	10, 15	ax-hbl1 103	. . . . . 6 |- T. |= [(\x:al \x:al By:al) = \x:al B]
23	16, 3, 15, 22, 20	hbc 110	. . . . 5 |- T. |= [(\x:al (\x:al Bz:al)y:al) = (\x:al Bz:al)]
24	14, 4, 15, 17, 18, 21, 23	hbov 111	. . . 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 64	. . . . . 6 |- x:al:al
27	2, 26	wc 50	. . . . 5 |- (\x:al Ax:al):be
28	16, 26	wc 50	. . . . 5 |- (\x:al Bx:al):be
29	26, 3	weqi 76	. . . . . . 7 |- [x:al = z:al]:*
30	29	id 25	. . . . . 6 |- [x:al = z:al] |= [x:al = z:al]
31	2, 26, 30	ceq2 90	. . . . 5 |- [x:al = z:al] |= [(\x:al Ax:al) = (\x:al Az:al)]
32	16, 26, 30	ceq2 90	. . . . 5 |- [x:al = z:al] |= [(\x:al Bx:al) = (\x:al Bz:al)]
33	14, 27, 28, 31, 32	oveq12 100	. . . 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 83	. . . 4 |- [x:al = z:al] |= [R = R]
35	13, 24, 25, 33, 34	ax-inst 113	. . 3 |- R |= [(\x:al Az:al) = (\x:al Bz:al)]
36	4, 35	leq 91	. 2 |- R |= [\z:al (\x:al Az:al) = \z:al (\x:al Bz:al)]
37	2	eta 178	. . 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 178	. . 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 97	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-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113  ax-eta 177

This theorem depends on definitions:  df-ov 73  df-al 126

This theorem is referenced by:  alrimi  182  axext  219  axrep  220