I am analysing axiomatic approach to defining real numbers. There are two axioms that postulate existence of $0$ and $1$, namely (according to my notes):
There exists an element $0\in\mathbb{R}$ such that for any $x\in\mathbb{R}$ we have $x+0=x.$
There exists an element $1\in\mathbb{R}$ such that for any $x\in\mathbb{R}$ we have $x\times 1=x$.
Then, I see a really little remark, almost non-existent, that says
We suppose $1\neq 0$.
I searched other sources which provided basically the same axioms but nowhere I could see the sentence $1\neq 0$ as an axiom.
My question is - why isn't it considered as an separate axiom? What it is then? I don't think you can prove it from other axioms of $\mathbb{R}$ and I think it is fairly important for the whole theory to work properly.
Yes, it should be considered an axiom (unless you are able to show it from the other axioms, for we definitely want $1\ne 0$ to hold).
In fact, you can easily present a model of all axioms[1] (except this), namely the set $\Bbb R=\{0\}$ (where $1$ is just another name for $0$) and the obvious operations.
[1] depends on your concrete list of axioms, of course