This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )