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 ≠ 0

Proof

Step	Hyp	Ref	Expression
1		1ne0sr	⊢ ¬ 1R = 0R
2		1sr	⊢ 1R ∈ R
3	2	elexi	⊢ 1R ∈ V
4	3	eqresr	⊢ ( ⟨ 1R , 0R ⟩ = ⟨ 0R , 0R ⟩ ↔ 1R = 0R )
5	1 4	mtbir	⊢ ¬ ⟨ 1R , 0R ⟩ = ⟨ 0R , 0R ⟩
6		df-1	⊢ 1 = ⟨ 1R , 0R ⟩
7		df-0	⊢ 0 = ⟨ 0R , 0R ⟩
8	6 7	eqeq12i	⊢ ( 1 = 0 ↔ ⟨ 1R , 0R ⟩ = ⟨ 0R , 0R ⟩ )
9	5 8	mtbir	⊢ ¬ 1 = 0
10	9	neir	⊢ 1 ≠ 0