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	⊢ (∀x x = y → ∀z w = v)

Distinct variable group:   x,y

Proof of Theorem aev

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

Syntax hints:   → wi 3  ∀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