Theorem axc11n-16 34223

Description: This theorem shows that, given ax-c16 34177, we can derive a version of ax-c11n 34173. However, it is weaker than ax-c11n 34173 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, z

Proof of Theorem axc11n-16

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-c16 34177	. . . 4 |- ( A. x x = z -> ( x = w -> A. x x = w ) )
2	1	alrimiv 1855	. . 3 |- ( A. x x = z -> A. w ( x = w -> A. x x = w ) )
3	2	axc4i-o 34183	. 2 |- ( A. x x = z -> A. x A. w ( x = w -> A. x x = w ) )
4		equequ1 1952	. . . . . 6 |- ( x = z -> ( x = w <-> z = w ) )
5	4	cbvalv 2273	. . . . . . 7 |- ( A. x x = w <-> A. z z = w )
6	5	a1i 11	. . . . . 6 |- ( x = z -> ( A. x x = w <-> A. z z = w ) )
7	4, 6	imbi12d 334	. . . . 5 |- ( x = z -> ( ( x = w -> A. x x = w ) <-> ( z = w -> A. z z = w ) ) )
8	7	albidv 1849	. . . 4 |- ( x = z -> ( A. w ( x = w -> A. x x = w ) <-> A. w ( z = w -> A. z z = w ) ) )
9	8	cbvalv 2273	. . 3 |- ( A. x A. w ( x = w -> A. x x = w ) <-> A. z A. w ( z = w -> A. z z = w ) )
10	9	biimpi 206	. 2 |- ( A. x A. w ( x = w -> A. x x = w ) -> A. z A. w ( z = w -> A. z z = w ) )
11		nfa1-o 34200	. . . . . . 7 |- F/ z A. z z = w
12	11	19.23 2080	. . . . . 6 |- ( A. z ( z = w -> A. z z = w ) <-> ( E. z z = w -> A. z z = w ) )
13	12	albii 1747	. . . . 5 |- ( A. w A. z ( z = w -> A. z z = w ) <-> A. w ( E. z z = w -> A. z z = w ) )
14		ax6ev 1890	. . . . . . . 8 |- E. z z = w
15		pm2.27 42	. . . . . . . 8 |- ( E. z z = w -> ( ( E. z z = w -> A. z z = w ) -> A. z z = w ) )
16	14, 15	ax-mp 5	. . . . . . 7 |- ( ( E. z z = w -> A. z z = w ) -> A. z z = w )
17	16	alimi 1739	. . . . . 6 |- ( A. w ( E. z z = w -> A. z z = w ) -> A. w A. z z = w )
18		equequ2 1953	. . . . . . . . 9 |- ( w = x -> ( z = w <-> z = x ) )
19	18	spv 2260	. . . . . . . 8 |- ( A. w z = w -> z = x )
20	19	sps-o 34193	. . . . . . 7 |- ( A. z A. w z = w -> z = x )
21	20	alcoms 2035	. . . . . 6 |- ( A. w A. z z = w -> z = x )
22	17, 21	syl 17	. . . . 5 |- ( A. w ( E. z z = w -> A. z z = w ) -> z = x )
23	13, 22	sylbi 207	. . . 4 |- ( A. w A. z ( z = w -> A. z z = w ) -> z = x )
24	23	alcoms 2035	. . 3 |- ( A. z A. w ( z = w -> A. z z = w ) -> z = x )
25	24	axc4i-o 34183	. 2 |- ( A. z A. w ( z = w -> A. z z = w ) -> A. z z = x )
26	3, 10, 25	3syl 18	1 |- ( A. x x = z -> A. z z = x )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-c5 34168  ax-c4 34169  ax-c7 34170  ax-c16 34177

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)