This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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