Theorem cbvf 167

Description: Change bound variables in a lambda abstraction.

Hypotheses

Ref	Expression
cbvf.1	|- A:be
cbvf.2	|- T. |= [(\y:al Az:al) = A]
cbvf.3	|- T. |= [(\x:al Bz:al) = B]
cbvf.4	|- [x:al = y:al] |= [A = B]

Assertion

Ref	Expression
cbvf	|- T. |= [\x:al A = \y:al B]

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

Proof of Theorem cbvf

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbvf.1	. . . . 5 |- A:be
2	1	wl 59	. . . 4 |- \x:al A:(al -> be)
3		wv 58	. . . 4 |- p:al:al
4	2, 3	wc 45	. . 3 |- (\x:al Ap:al):be
5	4	wl 59	. 2 |- \p:al (\x:al Ap:al):(al -> be)
6		cbvf.4	. . . . . . . 8 |- [x:al = y:al] |= [A = B]
7	1, 6	eqtypi 69	. . . . . . 7 |- B:be
8	7	wl 59	. . . . . 6 |- \y:al B:(al -> be)
9	8, 3	wc 45	. . . . 5 |- (\y:al Bp:al):be
10	4, 9	weqi 68	. . . 4 |- [(\x:al Ap:al) = (\y:al Bp:al)]:*
11		wv 58	. . . . 5 |- y:al:al
12		cbvf.3	. . . . 5 |- T. |= [(\x:al Bz:al) = B]
13		wv 58	. . . . . 6 |- z:al:al
14	11, 13	ax-17 95	. . . . 5 |- T. |= [(\x:al y:alz:al) = y:al]
15	1, 11, 6, 12, 14	clf 105	. . . 4 |- T. |= [(\x:al Ay:al) = B]
16		weq 38	. . . . 5 |- = :(be -> (be -> *))
17	16, 13	ax-17 95	. . . . 5 |- T. |= [(\y:al = z:al) = = ]
18		cbvf.2	. . . . . . 7 |- T. |= [(\y:al Az:al) = A]
19	1, 13, 18	hbl 102	. . . . . 6 |- T. |= [(\y:al \x:al Az:al) = \x:al A]
20	3, 13	ax-17 95	. . . . . 6 |- T. |= [(\y:al p:alz:al) = p:al]
21	2, 3, 13, 19, 20	hbc 100	. . . . 5 |- T. |= [(\y:al (\x:al Ap:al)z:al) = (\x:al Ap:al)]
22	18	ax-cb1 29	. . . . . . 7 |- T.:*
23	7, 13, 22	hbl1 94	. . . . . 6 |- T. |= [(\y:al \y:al Bz:al) = \y:al B]
24	8, 3, 13, 23, 20	hbc 100	. . . . 5 |- T. |= [(\y:al (\y:al Bp:al)z:al) = (\y:al Bp:al)]
25	16, 4, 13, 9, 17, 21, 24	hbov 101	. . . 4 |- T. |= [(\y:al [(\x:al Ap:al) = (\y:al Bp:al)]z:al) = [(\x:al Ap:al) = (\y:al Bp:al)]]
26	2, 11	wc 45	. . . . 5 |- (\x:al Ay:al):be
27	11, 3	weqi 68	. . . . . . 7 |- [y:al = p:al]:*
28	27	id 25	. . . . . 6 |- [y:al = p:al] |= [y:al = p:al]
29	2, 11, 28	ceq2 80	. . . . 5 |- [y:al = p:al] |= [(\x:al Ay:al) = (\x:al Ap:al)]
30	29	ax-cb1 29	. . . . . . 7 |- [y:al = p:al]:*
31	8, 11	wc 45	. . . . . . . 8 |- (\y:al By:al):be
32	7	beta 82	. . . . . . . 8 |- T. |= [(\y:al By:al) = B]
33	31, 32	eqcomi 70	. . . . . . 7 |- T. |= [B = (\y:al By:al)]
34	30, 33	a1i 28	. . . . . 6 |- [y:al = p:al] |= [B = (\y:al By:al)]
35	8, 11, 28	ceq2 80	. . . . . 6 |- [y:al = p:al] |= [(\y:al By:al) = (\y:al Bp:al)]
36	7, 34, 35	eqtri 85	. . . . 5 |- [y:al = p:al] |= [B = (\y:al Bp:al)]
37	16, 26, 7, 29, 36	oveq12 90	. . . 4 |- [y:al = p:al] |= [[(\x:al Ay:al) = B] = [(\x:al Ap:al) = (\y:al Bp:al)]]
38	3, 10, 15, 25, 37	insti 104	. . 3 |- T. |= [(\x:al Ap:al) = (\y:al Bp:al)]
39	4, 38	leq 81	. 2 |- T. |= [\p:al (\x:al Ap:al) = \p:al (\y:al Bp:al)]
40	2	eta 166	. 2 |- T. |= [\p:al (\x:al Ap:al) = \x:al A]
41	8	eta 166	. 2 |- T. |= [\p:al (\y:al Bp:al) = \y:al B]
42	5, 39, 40, 41	3eqtr3i 87	1 |- T. |= [\x:al A = \y: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-distrl 63  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:  cbv  168