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 ⊢∀xx=z→∀zz=x

Proof

Step Hyp Ref Expression
1 ax-c16 ⊢∀xx=z→x=w→∀xx=w
2 1 alrimiv ⊢∀xx=z→∀wx=w→∀xx=w
3 2 axc4i-o ⊢∀xx=z→∀x∀wx=w→∀xx=w
4 equequ1 ⊢x=z→x=w↔z=w
5 4 cbvalvw ⊢∀xx=w↔∀zz=w
6 5 a1i ⊢x=z→∀xx=w↔∀zz=w
7 4 6 imbi12d ⊢x=z→x=w→∀xx=w↔z=w→∀zz=w
8 7 albidv ⊢x=z→∀wx=w→∀xx=w↔∀wz=w→∀zz=w
9 8 cbvalvw ⊢∀x∀wx=w→∀xx=w↔∀z∀wz=w→∀zz=w
10 9 biimpi ⊢∀x∀wx=w→∀xx=w→∀z∀wz=w→∀zz=w
11 nfa1-o ⊢Ⅎz∀zz=w
12 11 19.23 ⊢∀zz=w→∀zz=w↔∃zz=w→∀zz=w
13 12 albii ⊢∀w∀zz=w→∀zz=w↔∀w∃zz=w→∀zz=w
14 ax6ev ⊢∃zz=w
15 pm2.27 ⊢∃zz=w→∃zz=w→∀zz=w→∀zz=w
16 14 15 ax-mp ⊢∃zz=w→∀zz=w→∀zz=w
17 16 alimi ⊢∀w∃zz=w→∀zz=w→∀w∀zz=w
18 equequ2 ⊢w=x→z=w↔z=x
19 18 spv ⊢∀wz=w→z=x
20 19 sps-o ⊢∀z∀wz=w→z=x
21 20 alcoms ⊢∀w∀zz=w→z=x
22 17 21 syl ⊢∀w∃zz=w→∀zz=w→z=x
23 13 22 sylbi ⊢∀w∀zz=w→∀zz=w→z=x
24 23 alcoms ⊢∀z∀wz=w→∀zz=w→z=x
25 24 axc4i-o ⊢∀z∀wz=w→∀zz=w→∀zz=x
26 3 10 25 3syl ⊢∀xx=z→∀zz=x