Theorem ax10ext 16364

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

Assertion

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

Distinct variable group:   x,z

Proof of Theorem ax10ext

Step	Hyp	Ref	Expression
1		ax-ext 1865	. . . . . 6 |- (A.w(w e. x <-> w e. z) -> x = z)
2	1	alimi 1338	. . . . 5 |- (A.xA.w(w e. x <-> w e. z) -> A.x x = z)
3		ax-14 1312	. . . . . . . . . 10 |- (x = z -> (w e. x -> w e. z))
4		idd 75	. . . . . . . . . 10 |- (x = z -> (A.x w e. x -> A.x w e. x))
5	3, 4	imim12d 69	. . . . . . . . 9 |- (x = z -> ((w e. z -> A.x w e. x) -> (w e. x -> A.x w e. x)))
6		bi2 166	. . . . . . . . . . 11 |- ((w e. x <-> w e. z) -> (w e. z -> w e. x))
7	6	alimi 1338	. . . . . . . . . 10 |- (A.x(w e. x <-> w e. z) -> A.x(w e. z -> w e. x))
8		ax-17 1317	. . . . . . . . . . 11 |- (w e. z -> A.x w e. z)
9	8	stdpc5 1405	. . . . . . . . . 10 |- (A.x(w e. z -> w e. x) -> (w e. z -> A.x w e. x))
10	7, 9	syl 12	. . . . . . . . 9 |- (A.x(w e. x <-> w e. z) -> (w e. z -> A.x w e. x))
11	5, 10	syl5 20	. . . . . . . 8 |- (x = z -> (A.x(w e. x <-> w e. z) -> (w e. x -> A.x w e. x)))
12	11	alimdv 1668	. . . . . . 7 |- (x = z -> (A.wA.x(w e. x <-> w e. z) -> A.w(w e. x -> A.x w e. x)))
13		ax-7 1304	. . . . . . 7 |- (A.xA.w(w e. x <-> w e. z) -> A.wA.x(w e. x <-> w e. z))
14	12, 13	syl5 20	. . . . . 6 |- (x = z -> (A.xA.w(w e. x <-> w e. z) -> A.w(w e. x -> A.x w e. x)))
15	14	a4s 1330	. . . . 5 |- (A.x x = z -> (A.xA.w(w e. x <-> w e. z) -> A.w(w e. x -> A.x w e. x)))
16	2, 15	mpcom 60	. . . 4 |- (A.xA.w(w e. x <-> w e. z) -> A.w(w e. x -> A.x w e. x))
17	16	a5i 1335	. . 3 |- (A.xA.w(w e. x <-> w e. z) -> A.xA.w(w e. x -> A.x w e. x))
18		hba1 1350	. . . . . . . 8 |- (A.x w e. x -> A.xA.x w e. x)
19	18	19.23 1411	. . . . . . 7 |- (A.x(w e. x -> A.x w e. x) <-> (E.x w e. x -> A.x w e. x))
20		19.8a 1376	. . . . . . . . 9 |- (w e. z -> E.z w e. z)
21		ax-17 1317	. . . . . . . . . 10 |- (w e. x -> A.z w e. x)
22		elequ2 1497	. . . . . . . . . 10 |- (z = x -> (w e. z <-> w e. x))
23	8, 21, 22	cbvex 1529	. . . . . . . . 9 |- (E.z w e. z <-> E.x w e. x)
24	20, 23	sylib 215	. . . . . . . 8 |- (w e. z -> E.x w e. x)
25	21, 8, 3	cbv3 1525	. . . . . . . 8 |- (A.x w e. x -> A.z w e. z)
26	24, 25	imim12i 21	. . . . . . 7 |- ((E.x w e. x -> A.x w e. x) -> (w e. z -> A.z w e. z))
27	19, 26	sylbi 216	. . . . . 6 |- (A.x(w e. x -> A.x w e. x) -> (w e. z -> A.z w e. z))
28	27	alimi 1338	. . . . 5 |- (A.wA.x(w e. x -> A.x w e. x) -> A.w(w e. z -> A.z w e. z))
29	28	a7s 1337	. . . 4 |- (A.xA.w(w e. x -> A.x w e. x) -> A.w(w e. z -> A.z w e. z))
30	29	19.21aiv 1664	. . 3 |- (A.xA.w(w e. x -> A.x w e. x) -> A.zA.w(w e. z -> A.z w e. z))
31		hba1 1350	. . . . . . . 8 |- (A.z w e. z -> A.zA.z w e. z)
32	31	19.23 1411	. . . . . . 7 |- (A.z(w e. z -> A.z w e. z) <-> (E.z w e. z -> A.z w e. z))
33		ax-14 1312	. . . . . . . . . . 11 |- (z = x -> (w e. z -> w e. x))
34	8, 21, 33	cbv3 1525	. . . . . . . . . 10 |- (A.z w e. z -> A.x w e. x)
35		ax-4 1319	. . . . . . . . . 10 |- (A.x w e. x -> w e. x)
36	34, 35	syl 12	. . . . . . . . 9 |- (A.z w e. z -> w e. x)
37	20, 36	imim12i 21	. . . . . . . 8 |- ((E.z w e. z -> A.z w e. z) -> (w e. z -> w e. x))
38		19.8a 1376	. . . . . . . . . 10 |- (w e. x -> E.x w e. x)
39		elequ2 1497	. . . . . . . . . . 11 |- (x = z -> (w e. x <-> w e. z))
40	21, 8, 39	cbvex 1529	. . . . . . . . . 10 |- (E.x w e. x <-> E.z w e. z)
41	38, 40	sylib 215	. . . . . . . . 9 |- (w e. x -> E.z w e. z)
42		ax-4 1319	. . . . . . . . 9 |- (A.z w e. z -> w e. z)
43	41, 42	imim12i 21	. . . . . . . 8 |- ((E.z w e. z -> A.z w e. z) -> (w e. x -> w e. z))
44	37, 43	impbid 574	. . . . . . 7 |- ((E.z w e. z -> A.z w e. z) -> (w e. z <-> w e. x))
45	32, 44	sylbi 216	. . . . . 6 |- (A.z(w e. z -> A.z w e. z) -> (w e. z <-> w e. x))
46	45	alimi 1338	. . . . 5 |- (A.wA.z(w e. z -> A.z w e. z) -> A.w(w e. z <-> w e. x))
47	46	a7s 1337	. . . 4 |- (A.zA.w(w e. z -> A.z w e. z) -> A.w(w e. z <-> w e. x))
48	47	a5i 1335	. . 3 |- (A.zA.w(w e. z -> A.z w e. z) -> A.zA.w(w e. z <-> w e. x))
49	17, 30, 48	3syl 24	. 2 |- (A.xA.w(w e. x <-> w e. z) -> A.zA.w(w e. z <-> w e. x))
50		axext4 1869	. . 3 |- (x = z <-> A.w(w e. x <-> w e. z))
51	50	albii 1346	. 2 |- (A.x x = z <-> A.xA.w(w e. x <-> w e. z))
52		axext4 1869	. . 3 |- (z = x <-> A.w(w e. z <-> w e. x))
53	52	albii 1346	. 2 |- (A.z z = x <-> A.zA.w(w e. z <-> w e. x))
54	49, 51, 53	3imtr4i 236	1 |- (A.x x = z -> A.z z = x)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300  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-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

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

Copyright terms: Public domain