leqf - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > leqf		Unicode version

Theorem leqf 169

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

**Assertion**
Ref	Expression
leqf

Proof of Theorem leqf Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		leqf.1	. . . . 5
2	1	wl 59	. . . 4
3		wv 58	. . . 4
4	2, 3	wc 45	. . 3
5	4	wl 59	. 2
6		leqf.2	. . . . 5
7	6	ax-cb1 29	. . . . . 6
8	1	beta 82	. . . . . 6
9	7, 8	a1i 28	. . . . 5
10	1, 6	eqtypi 69	. . . . . . 7
11	10	beta 82	. . . . . 6
12	7, 11	a1i 28	. . . . 5
13	1, 6, 9, 12	3eqtr4i 86	. . . 4
14		weq 38	. . . . 5
15		wv 58	. . . . 5
16	10	wl 59	. . . . . 6
17	16, 3	wc 45	. . . . 5
18	14, 15	ax-17 95	. . . . 5
19	1, 15	ax-hbl1 93	. . . . . 6
20	3, 15	ax-17 95	. . . . . 6
21	2, 3, 15, 19, 20	hbc 100	. . . . 5
22	10, 15	ax-hbl1 93	. . . . . 6
23	16, 3, 15, 22, 20	hbc 100	. . . . 5
24	14, 4, 15, 17, 18, 21, 23	hbov 101	. . . 4
25		leqf.3	. . . 4
26		wv 58	. . . . . 6
27	2, 26	wc 45	. . . . 5
28	16, 26	wc 45	. . . . 5
29	26, 3	weqi 68	. . . . . . 7
30	29	id 25	. . . . . 6
31	2, 26, 30	ceq2 80	. . . . 5
32	16, 26, 30	ceq2 80	. . . . 5
33	14, 27, 28, 31, 32	oveq12 90	. . . 4
34	29, 7	eqid 73	. . . 4
35	13, 24, 25, 33, 34	ax-inst 103	. . 3
36	4, 35	leq 81	. 2
37	2	eta 166	. . 3
38	7, 37	a1i 28	. 2
39	16	eta 166	. . 3
40	7, 39	a1i 28	. 2
41	5, 36, 38, 40	3eqtr3i 87	1

Colors of variables: type var term

Syntax hints: tv 1

ht 2

hb 3 kc 5

kl 6

ke 7

kt 8

kbr 9

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