Theorem ax1ne0

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 . (Contributed by NM, 19-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	ax1ne0	$$⊢1\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		1ne0sr	$$⊢\neg 1_{𝑹}=0_{𝑹}$$
2		1sr	$$⊢1_{𝑹}\in 𝑹$$
3	2	elexi	$$⊢1_{𝑹}\in \mathrm{V}$$
4	3	eqresr	$$⊢⟨1_{𝑹},0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩\leftrightarrow 1_{𝑹}=0_{𝑹}$$
5	1 4	mtbir	$$⊢\neg ⟨1_{𝑹},0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩$$
6		df-1	$$⊢1=⟨1_{𝑹},0_{𝑹}⟩$$
7		df-0	$$⊢0=⟨0_{𝑹},0_{𝑹}⟩$$
8	6 7	eqeq12i	$$⊢1=0\leftrightarrow ⟨1_{𝑹},0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩$$
9	5 8	mtbir	$$⊢\neg 1=0$$
10	9	neir	$$⊢1\ne 0$$