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:β
leqf.2	⊢ R⊧[A = B]
leqf.3	⊢ ⊤⊧[(λx:α Ry:α) = R]

Assertion

Ref	Expression
leqf	⊢ R⊧[λx:α A = λx:α B]

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

Proof of Theorem leqf

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		leqf.1	. . . . 5 ⊢ A:β
2	1	wl 66	. . . 4 ⊢ λx:α A:(α → β)
3		wv 64	. . . 4 ⊢ z:α:α
4	2, 3	wc 50	. . 3 ⊢ (λx:α Az:α):β
5	4	wl 66	. 2 ⊢ λz:α (λx:α Az:α):(α → β)
6		leqf.2	. . . . 5 ⊢ R⊧[A = B]
7	6	ax-cb1 29	. . . . . 6 ⊢ R:∗
8	1	beta 92	. . . . . 6 ⊢ ⊤⊧[(λx:α Ax:α) = A]
9	7, 8	a1i 28	. . . . 5 ⊢ R⊧[(λx:α Ax:α) = A]
10	1, 6	eqtypi 78	. . . . . . 7 ⊢ B:β
11	10	beta 92	. . . . . 6 ⊢ ⊤⊧[(λx:α Bx:α) = B]
12	7, 11	a1i 28	. . . . 5 ⊢ R⊧[(λx:α Bx:α) = B]
13	1, 6, 9, 12	3eqtr4i 96	. . . 4 ⊢ R⊧[(λx:α Ax:α) = (λx:α Bx:α)]
14		weq 41	. . . . 5 ⊢ = :(β → (β → ∗))
15		wv 64	. . . . 5 ⊢ y:α:α
16	10	wl 66	. . . . . 6 ⊢ λx:α B:(α → β)
17	16, 3	wc 50	. . . . 5 ⊢ (λx:α Bz:α):β
18	14, 15	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:α = y:α) = = ]
19	1, 15	ax-hbl1 103	. . . . . 6 ⊢ ⊤⊧[(λx:α λx:α Ay:α) = λx:α A]
20	3, 15	ax-17 105	. . . . . 6 ⊢ ⊤⊧[(λx:α z:αy:α) = z:α]
21	2, 3, 15, 19, 20	hbc 110	. . . . 5 ⊢ ⊤⊧[(λx:α (λx:α Az:α)y:α) = (λx:α Az:α)]
22	10, 15	ax-hbl1 103	. . . . . 6 ⊢ ⊤⊧[(λx:α λx:α By:α) = λx:α B]
23	16, 3, 15, 22, 20	hbc 110	. . . . 5 ⊢ ⊤⊧[(λx:α (λx:α Bz:α)y:α) = (λx:α Bz:α)]
24	14, 4, 15, 17, 18, 21, 23	hbov 111	. . . 4 ⊢ ⊤⊧[(λx:α [(λx:α Az:α) = (λx:α Bz:α)]y:α) = [(λx:α Az:α) = (λx:α Bz:α)]]
25		leqf.3	. . . 4 ⊢ ⊤⊧[(λx:α Ry:α) = R]
26		wv 64	. . . . . 6 ⊢ x:α:α
27	2, 26	wc 50	. . . . 5 ⊢ (λx:α Ax:α):β
28	16, 26	wc 50	. . . . 5 ⊢ (λx:α Bx:α):β
29	26, 3	weqi 76	. . . . . . 7 ⊢ [x:α = z:α]:∗
30	29	id 25	. . . . . 6 ⊢ [x:α = z:α]⊧[x:α = z:α]
31	2, 26, 30	ceq2 90	. . . . 5 ⊢ [x:α = z:α]⊧[(λx:α Ax:α) = (λx:α Az:α)]
32	16, 26, 30	ceq2 90	. . . . 5 ⊢ [x:α = z:α]⊧[(λx:α Bx:α) = (λx:α Bz:α)]
33	14, 27, 28, 31, 32	oveq12 100	. . . 4 ⊢ [x:α = z:α]⊧[[(λx:α Ax:α) = (λx:α Bx:α)] = [(λx:α Az:α) = (λx:α Bz:α)]]
34	29, 7	eqid 83	. . . 4 ⊢ [x:α = z:α]⊧[R = R]
35	13, 24, 25, 33, 34	ax-inst 113	. . 3 ⊢ R⊧[(λx:α Az:α) = (λx:α Bz:α)]
36	4, 35	leq 91	. 2 ⊢ R⊧[λz:α (λx:α Az:α) = λz:α (λx:α Bz:α)]
37	2	eta 178	. . 3 ⊢ ⊤⊧[λz:α (λx:α Az:α) = λx:α A]
38	7, 37	a1i 28	. 2 ⊢ R⊧[λz:α (λx:α Az:α) = λx:α A]
39	16	eta 178	. . 3 ⊢ ⊤⊧[λz:α (λx:α Bz:α) = λx:α B]
40	7, 39	a1i 28	. 2 ⊢ R⊧[λz:α (λx:α Bz:α) = λx:α B]
41	5, 36, 38, 40	3eqtr3i 97	1 ⊢ R⊧[λx:α A = λx:α B]

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤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