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	|- ( ( ( N e. NN /\ A e. ( EE ` N ) ) /\ ( M e. NN /\ A e. ( EE ` M ) ) ) -> N = M )

Proof

Step	Hyp	Ref	Expression
1		eedimeq	|- ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> N = M )
2	1	ad2ant2l	|- ( ( ( N e. NN /\ A e. ( EE ` N ) ) /\ ( M e. NN /\ A e. ( EE ` M ) ) ) -> N = M )