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

Metamath Proof Explorer

Axiom ax-1ne0

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 . (Contributed by NM, 29-Jan-1995)

Ref Expression
Assertion ax-1ne0 ⊢ 1 ≠ 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1 class 1
1 cc0 class 0
2 0 1 wne wff 1 ≠ 0