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

Proof

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