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 ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 𝑧 = 𝑥 )

Proof

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