Theorem aev 1577

Description: A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1580. (The proof was shortened by Andrew Salmon, 21-Jun-2011.)

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 1505	. 2 |- (A.x x = y -> A.zA.x x = y)
2		hbae 1505	. . . 4 |- (A.x x = y -> A.fA.x x = y)
3		ax-8 1306	. . . . 5 |- (x = f -> (x = y -> f = y))
4	3	a4imv 1576	. . . 4 |- (A.x x = y -> f = y)
5	2, 4	19.21ai 1345	. . 3 |- (A.x x = y -> A.f f = y)
6		ax-8 1306	. . . . . . . 8 |- (y = u -> (y = f -> u = f))
7		equcomi 1487	. . . . . . . 8 |- (u = f -> f = u)
8	6, 7	syl6 25	. . . . . . 7 |- (y = u -> (y = f -> f = u))
9	8	a4imv 1576	. . . . . 6 |- (A.y y = f -> f = u)
10	9	alequcoms 1503	. . . . 5 |- (A.f f = y -> f = u)
11	10	a5i 1335	. . . 4 |- (A.f f = y -> A.f f = u)
12		hbae 1505	. . . . 5 |- (A.f f = u -> A.vA.f f = u)
13		ax-8 1306	. . . . . 6 |- (f = v -> (f = u -> v = u))
14	13	a4imv 1576	. . . . 5 |- (A.f f = u -> v = u)
15	12, 14	19.21ai 1345	. . . 4 |- (A.f f = u -> A.v v = u)
16		alequcom 1502	. . . 4 |- (A.v v = u -> A.u u = v)
17	11, 15, 16	3syl 24	. . 3 |- (A.f f = y -> A.u u = v)
18		ax-8 1306	. . . 4 |- (u = w -> (u = v -> w = v))
19	18	a4imv 1576	. . 3 |- (A.u u = v -> w = v)
20	5, 17, 19	3syl 24	. 2 |- (A.x x = y -> w = v)
21	1, 20	19.21ai 1345	1 |- (A.x x = y -> A.z w = v)

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

This theorem is referenced by:  ax16 1579  a16g 1653

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