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

Metamath Proof Explorer

Theorem axc11n-16

Proof