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 )