Theorem aevOLD 1578

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1580. The proof is unusual in that it involves linking 17 implications, which might provide an interesting challenge for an automated theorem prover.

Assertion

Ref	Expression
aevOLD	|- (A.x x = y -> A.z w = v)

Distinct variable group:   x,y

Proof of Theorem aevOLD

Step	Hyp	Ref	Expression
1		hbae 1505	. 2 |- (A.x x = y -> A.zA.x x = y)
2		hbae 1505	. . . 4 |- (A.x x = y -> A.xA.x x = y)
3		alequcom 1502	. . . . . 6 |- (A.x x = y -> A.y y = x)
4		ax-8 1306	. . . . . . 7 |- (y = u -> (y = x -> u = x))
5	4	a4imv 1576	. . . . . 6 |- (A.y y = x -> u = x)
6		equcomi 1487	. . . . . 6 |- (u = x -> x = u)
7	3, 5, 6	3syl 24	. . . . 5 |- (A.x x = y -> x = u)
8	7	alimi 1338	. . . 4 |- (A.xA.x x = y -> A.x x = u)
9		alequcom 1502	. . . . 5 |- (A.x x = u -> A.u u = x)
10		alequcom 1502	. . . . . . 7 |- (A.u u = x -> A.x x = u)
11		ax-8 1306	. . . . . . . 8 |- (x = f -> (x = u -> f = u))
12	11	a4imv 1576	. . . . . . 7 |- (A.x x = u -> f = u)
13		equcomi 1487	. . . . . . 7 |- (f = u -> u = f)
14	10, 12, 13	3syl 24	. . . . . 6 |- (A.u u = x -> u = f)
15	14	a5i 1335	. . . . 5 |- (A.u u = x -> A.u u = f)
16		hbae 1505	. . . . . 6 |- (A.u u = f -> A.uA.u u = f)
17		alequcom 1502	. . . . . . . 8 |- (A.u u = f -> A.f f = u)
18		ax-8 1306	. . . . . . . . 9 |- (f = v -> (f = u -> v = u))
19	18	a4imv 1576	. . . . . . . 8 |- (A.f f = u -> v = u)
20		equcomi 1487	. . . . . . . 8 |- (v = u -> u = v)
21	17, 19, 20	3syl 24	. . . . . . 7 |- (A.u u = f -> u = v)
22	21	alimi 1338	. . . . . 6 |- (A.uA.u u = f -> A.u u = v)
23		alequcom 1502	. . . . . . 7 |- (A.u u = v -> A.v v = u)
24		alequcom 1502	. . . . . . . . 9 |- (A.v v = u -> A.u u = v)
25		ax-8 1306	. . . . . . . . . 10 |- (u = w -> (u = v -> w = v))
26	25	a4imv 1576	. . . . . . . . 9 |- (A.u u = v -> w = v)
27		equcomi 1487	. . . . . . . . 9 |- (w = v -> v = w)
28	24, 26, 27	3syl 24	. . . . . . . 8 |- (A.v v = u -> v = w)
29	28	a5i 1335	. . . . . . 7 |- (A.v v = u -> A.v v = w)
30		alequcom 1502	. . . . . . 7 |- (A.v v = w -> A.w w = v)
31	23, 29, 30	3syl 24	. . . . . 6 |- (A.u u = v -> A.w w = v)
32	16, 22, 31	3syl 24	. . . . 5 |- (A.u u = f -> A.w w = v)
33	9, 15, 32	3syl 24	. . . 4 |- (A.x x = u -> A.w w = v)
34	2, 8, 33	3syl 24	. . 3 |- (A.x x = y -> A.w w = v)
35	34	19.21bi 1408	. 2 |- (A.x x = y -> w = v)
36	1, 35	19.21ai 1345	1 |- (A.x x = y -> A.z w = v)

Syntax hints:   -> wi 3  A.wal 1296   = wceq 1298

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500

Copyright terms: Public domain