Theorem axc11n-16

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-c16	|- ( A. x x = z -> ( x = w -> A. x x = w ) )
2	1	alrimiv	|- ( A. x x = z -> A. w ( x = w -> A. x x = w ) )
3	2	axc4i-o	|- ( A. x x = z -> A. x A. w ( x = w -> A. x x = w ) )
4		equequ1	|- ( x = z -> ( x = w <-> z = w ) )
5	4	cbvalvw	|- ( A. x x = w <-> A. z z = w )
6	5	a1i	|- ( x = z -> ( A. x x = w <-> A. z z = w ) )
7	4 6	imbi12d	|- ( x = z -> ( ( x = w -> A. x x = w ) <-> ( z = w -> A. z z = w ) ) )
8	7	albidv	|- ( x = z -> ( A. w ( x = w -> A. x x = w ) <-> A. w ( z = w -> A. z z = w ) ) )
9	8	cbvalvw	|- ( A. x A. w ( x = w -> A. x x = w ) <-> A. z A. w ( z = w -> A. z z = w ) )
10	9	biimpi	|- ( A. x A. w ( x = w -> A. x x = w ) -> A. z A. w ( z = w -> A. z z = w ) )
11		nfa1-o	|- F/ z A. z z = w
12	11	19.23	|- ( A. z ( z = w -> A. z z = w ) <-> ( E. z z = w -> A. z z = w ) )
13	12	albii	|- ( A. w A. z ( z = w -> A. z z = w ) <-> A. w ( E. z z = w -> A. z z = w ) )
14		ax6ev	|- E. z z = w
15		pm2.27	|- ( E. z z = w -> ( ( E. z z = w -> A. z z = w ) -> A. z z = w ) )
16	14 15	ax-mp	|- ( ( E. z z = w -> A. z z = w ) -> A. z z = w )
17	16	alimi	|- ( A. w ( E. z z = w -> A. z z = w ) -> A. w A. z z = w )
18		equequ2	|- ( w = x -> ( z = w <-> z = x ) )
19	18	spv	|- ( A. w z = w -> z = x )
20	19	sps-o	|- ( A. z A. w z = w -> z = x )
21	20	alcoms	|- ( A. w A. z z = w -> z = x )
22	17 21	syl	|- ( A. w ( E. z z = w -> A. z z = w ) -> z = x )
23	13 22	sylbi	|- ( A. w A. z ( z = w -> A. z z = w ) -> z = x )
24	23	alcoms	|- ( A. z A. w ( z = w -> A. z z = w ) -> z = x )
25	24	axc4i-o	|- ( A. z A. w ( z = w -> A. z z = w ) -> A. z z = x )
26	3 10 25	3syl	|- ( A. x x = z -> A. z z = x )