¿Spivak usa una propiedad en su propia prueba?

Estoy leyendo Cálculo de Spivak, 4.ª edición y en el Capítulo 1: Propiedades básicas de los números. Tengo problemas para entender una prueba de una de esas propiedades básicas.

Primero establece 3 propiedades básicas:

1. $a + (b + c) = (a + b) + c$
2. $a + 0 = 0 + a = a$
3. $a + (-a) = (-a) + a = 0$

Aquí cito a Spivak:

La propiedad P2 debería representar una característica distintiva del número$0$, y es reconfortante notar que ya estamos en condiciones de demostrarlo. De hecho, si un número$x$satisface

$$a+x=a$$ para cualquier número$a$, entonces$x = 0$(y en consecuencia esta ecuación también es válida para todos los números$a$). La prueba de esta afirmación implica nada más que restar$a$de ambos lados de la ecuación, es decir, sumando$-a$a ambos lados; como muestra la siguiente prueba detallada, las tres propiedades P1—P3 deben usarse para justificar esta operación. $$\begin{equation} \begin{split} &\text{If } \qquad\qquad\qquad\: a+x=a, \\ &\text{then }\qquad(-a)+(a+x)=(-a)+a=0; \\ &\text{hence } \:\:\quad ((-a)+a)+x=0; \\ &\text{hence } \:\:\,\,\qquad\qquad 0+x=0; \\ &\text{hence } \qquad\qquad\qquad\,\, x=0. \ \end{split} \end{equation}$$

Por lo que entendí, esta es una prueba de la segunda propiedad, pero él establece explícitamente que la segunda propiedad debe usarse en la prueba. No puedo ver cómo se puede justificar esto y me resulta frustrante descifrar la lógica detrás de esta prueba. ¿Puede alguien señalar dónde me estoy equivocando porque confío en que es un error de mi parte en lugar de un error en el libro de texto, lo cual es difícil de creer considerando las muchas ediciones por las que ha pasado el libro y es raro para un autor? del calibre de Spivak.

Además, una propiedad como esta no se consideraría simplemente como un axioma de algún conjunto de números, como los anteriores, ¿cómo se sabe si una propiedad tan básica puede incluso probarse?

Encontré esta pregunta relevante. ¿La prueba dada muestra que 0 es la identidad aditiva única? , pero la respuesta parece señalar que Spivak no lo prueba, sino que lo estipula a través de P2, lo que parece extraño ya que el propio Spivak afirma que está probado.

Disculpas de antemano si he cometido un error u omisión vergonzoso, este libro no es una lectura fácil para mí.