Theorem axdimuniq

Description: The unique dimension axiom. If a point is in N dimensional space and in M dimensional space, then N = M . This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013)

	Ref	Expression
Assertion	axdimuniq	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) ) → 𝑁 = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		eedimeq	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → 𝑁 = 𝑀 )
2	1	ad2ant2l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) ) → 𝑁 = 𝑀 )