Theorem aev 1192

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1194. 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 1128	. 2 |- (A.x x = y -> A.zA.x x = y)
2		hbae 1128	. . . 4 |- (A.x x = y -> A.xA.x x = y)
3		alequcom 1125	. . . . . 6 |- (A.x x = y -> A.y y = x)
4		ax-8 1101	. . . . . . 7 |- (y = u -> (y = x -> u = x))
5	4	a4b 1191	. . . . . 6 |- (A.y y = x -> u = x)
6		equcomi 1115	. . . . . 6 |- (u = x -> x = u)
7	3, 5, 6	3syl 20	. . . . 5 |- (A.x x = y -> x = u)
8	7	19.20i 968	. . . 4 |- (A.xA.x x = y -> A.x x = u)
9		alequcom 1125	. . . . 5 |- (A.x x = u -> A.u u = x)
10		alequcom 1125	. . . . . . 7 |- (A.u u = x -> A.x x = u)
11		ax-8 1101	. . . . . . . 8 |- (x = f -> (x = u -> f = u))
12	11	a4b 1191	. . . . . . 7 |- (A.x x = u -> f = u)
13		equcomi 1115	. . . . . . 7 |- (f = u -> u = f)
14	10, 12, 13	3syl 20	. . . . . 6 |- (A.u u = x -> u = f)
15	14	a5i 965	. . . . 5 |- (A.u u = x -> A.u u = f)
16		hbae 1128	. . . . . 6 |- (A.u u = f -> A.uA.u u = f)
17		alequcom 1125	. . . . . . . 8 |- (A.u u = f -> A.f f = u)
18		ax-8 1101	. . . . . . . . 9 |- (f = v -> (f = u -> v = u))
19	18	a4b 1191	. . . . . . . 8 |- (A.f f = u -> v = u)
20		equcomi 1115	. . . . . . . 8 |- (v = u -> u = v)
21	17, 19, 20	3syl 20	. . . . . . 7 |- (A.u u = f -> u = v)
22	21	19.20i 968	. . . . . 6 |- (A.uA.u u = f -> A.u u = v)
23		alequcom 1125	. . . . . . 7 |- (A.u u = v -> A.v v = u)
24		alequcom 1125	. . . . . . . . 9 |- (A.v v = u -> A.u u = v)
25		ax-8 1101	. . . . . . . . . 10 |- (u = w -> (u = v -> w = v))
26	25	a4b 1191	. . . . . . . . 9 |- (A.u u = v -> w = v)
27		equcomi 1115	. . . . . . . . 9 |- (w = v -> v = w)
28	24, 26, 27	3syl 20	. . . . . . . 8 |- (A.v v = u -> v = w)
29	28	a5i 965	. . . . . . 7 |- (A.v v = u -> A.v v = w)
30		alequcom 1125	. . . . . . 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 1036	. 2 |- (A.x x = y -> w = v)
36	1, 35	19.21ai 974	1 |- (A.x x = y -> A.z w = v)

Syntax hints:   -> wi 3  A.wal 950   = wceq 1099

This theorem is referenced by:  ax16 1193

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain