Theorem ax10-16 16365

Description: This theorem shows that, given ax-16 1580, ax-10 1308 is logically redundant.

Assertion

Ref	Expression
ax10-16	|- (A.x x = z -> A.z z = x)

Distinct variable group:   x,z

Proof of Theorem ax10-16

Step	Hyp	Ref	Expression
1		ax-16 1580	. . . 4 |- (A.x x = z -> (x = w -> A.x x = w))
2	1	19.21aiv 1664	. . 3 |- (A.x x = z -> A.w(x = w -> A.x x = w))
3	2	a5i 1335	. 2 |- (A.x x = z -> A.xA.w(x = w -> A.x x = w))
4		equequ1 1494	. . . . . 6 |- (x = z -> (x = w <-> z = w))
5	4	cbvalv 1696	. . . . . . 7 |- (A.x x = w <-> A.z z = w)
6	5	a1i 8	. . . . . 6 |- (x = z -> (A.x x = w <-> A.z z = w))
7	4, 6	imbi12d 688	. . . . 5 |- (x = z -> ((x = w -> A.x x = w) <-> (z = w -> A.z z = w)))
8	7	albidv 1656	. . . 4 |- (x = z -> (A.w(x = w -> A.x x = w) <-> A.w(z = w -> A.z z = w)))
9	8	cbvalv 1696	. . 3 |- (A.xA.w(x = w -> A.x x = w) <-> A.zA.w(z = w -> A.z z = w))
10	9	biimpi 168	. 2 |- (A.xA.w(x = w -> A.x x = w) -> A.zA.w(z = w -> A.z z = w))
11		hba1 1350	. . . . . . 7 |- (A.z z = w -> A.zA.z z = w)
12	11	19.23 1411	. . . . . 6 |- (A.z(z = w -> A.z z = w) <-> (E.z z = w -> A.z z = w))
13	12	albii 1346	. . . . 5 |- (A.wA.z(z = w -> A.z z = w) <-> A.w(E.z z = w -> A.z z = w))
14		a9e 1483	. . . . . . . 8 |- E.z z = w
15		pm2.27 76	. . . . . . . 8 |- (E.z z = w -> ((E.z z = w -> A.z z = w) -> A.z z = w))
16	14, 15	ax-mp 7	. . . . . . 7 |- ((E.z z = w -> A.z z = w) -> A.z z = w)
17	16	alimi 1338	. . . . . 6 |- (A.w(E.z z = w -> A.z z = w) -> A.wA.z z = w)
18		equequ2 1495	. . . . . . . . . 10 |- (w = x -> (z = w <-> z = x))
19	18	cbvalv 1696	. . . . . . . . 9 |- (A.w z = w <-> A.x z = x)
20		ax-4 1319	. . . . . . . . 9 |- (A.x z = x -> z = x)
21	19, 20	sylbi 216	. . . . . . . 8 |- (A.w z = w -> z = x)
22	21	a4s 1330	. . . . . . 7 |- (A.zA.w z = w -> z = x)
23	22	a7s 1337	. . . . . 6 |- (A.wA.z z = w -> z = x)
24	17, 23	syl 12	. . . . 5 |- (A.w(E.z z = w -> A.z z = w) -> z = x)
25	13, 24	sylbi 216	. . . 4 |- (A.wA.z(z = w -> A.z z = w) -> z = x)
26	25	a7s 1337	. . 3 |- (A.zA.w(z = w -> A.z z = w) -> z = x)
27	26	a5i 1335	. 2 |- (A.zA.w(z = w -> A.z z = w) -> A.z z = x)
28	3, 10, 27	3syl 24	1 |- (A.x x = z -> A.z z = x)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298  E.wex 1326

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-9 1307  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-16 1580

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain