Theorem aev 1206

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1208. 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
aev	|- (A.x x = y -> A.z w = v)

Distinct variable group:   x,y

Proof of Theorem aev

Step	Hyp	Ref	Expression
1		hbae 1143	. 2 |- (A.x x = y -> A.zA.x x = y)
2		hbae 1143	. . . 4 |- (A.x x = y -> A.xA.x x = y)
3		alequcom 1140	. . . . . 6 |- (A.x x = y -> A.y y = x)
4		ax-8 962	. . . . . . 7 |- (y = u -> (y = x -> u = x))
5	4	a4imv 1205	. . . . . 6 |- (A.y y = x -> u = x)
6		equcomi 1126	. . . . . 6 |- (u = x -> x = u)
7	3, 5, 6	3syl 20	. . . . 5 |- (A.x x = y -> x = u)
8	7	19.20i 990	. . . 4 |- (A.xA.x x = y -> A.x x = u)
9		alequcom 1140	. . . . 5 |- (A.x x = u -> A.u u = x)
10		alequcom 1140	. . . . . . 7 |- (A.u u = x -> A.x x = u)
11		ax-8 962	. . . . . . . 8 |- (x = f -> (x = u -> f = u))
12	11	a4imv 1205	. . . . . . 7 |- (A.x x = u -> f = u)
13		equcomi 1126	. . . . . . 7 |- (f = u -> u = f)
14	10, 12, 13	3syl 20	. . . . . 6 |- (A.u u = x -> u = f)
15	14	a5i 987	. . . . 5 |- (A.u u = x -> A.u u = f)
16		hbae 1143	. . . . . 6 |- (A.u u = f -> A.uA.u u = f)
17		alequcom 1140	. . . . . . . 8 |- (A.u u = f -> A.f f = u)
18		ax-8 962	. . . . . . . . 9 |- (f = v -> (f = u -> v = u))
19	18	a4imv 1205	. . . . . . . 8 |- (A.f f = u -> v = u)
20		equcomi 1126	. . . . . . . 8 |- (v = u -> u = v)
21	17, 19, 20	3syl 20	. . . . . . 7 |- (A.u u = f -> u = v)
22	21	19.20i 990	. . . . . 6 |- (A.uA.u u = f -> A.u u = v)
23		alequcom 1140	. . . . . . 7 |- (A.u u = v -> A.v v = u)
24		alequcom 1140	. . . . . . . . 9 |- (A.v v = u -> A.u u = v)
25		ax-8 962	. . . . . . . . . 10 |- (u = w -> (u = v -> w = v))
26	25	a4imv 1205	. . . . . . . . 9 |- (A.u u = v -> w = v)
27		equcomi 1126	. . . . . . . . 9 |- (w = v -> v = w)
28	24, 26, 27	3syl 20	. . . . . . . 8 |- (A.v v = u -> v = w)
29	28	a5i 987	. . . . . . 7 |- (A.v v = u -> A.v v = w)
30		alequcom 1140	. . . . . . 7 |- (A.v v = w -> A.w w = v)
31	23, 29, 30	3syl 20	. . . . . 6 |- (A.u u = v -> A.w w = v)
32	16, 22, 31	3syl 20	. . . . 5 |- (A.u u = f -> A.w w = v)
33	9, 15, 32	3syl 20	. . . 4 |- (A.x x = u -> A.w w = v)
34	2, 8, 33	3syl 20	. . 3 |- (A.x x = y -> A.w w = v)
35	34	19.21bi 1058	. 2 |- (A.x x = y -> w = v)
36	1, 35	19.21ai 996	1 |- (A.x x = y -> A.z w = v)

Syntax hints:   -> wi 3  A.wal 952   = wceq 954

This theorem is referenced by:  ax16 1207

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138

Copyright terms: Public domain