It would be somewhat lengthy to explain its meaning exactly here. You can read about its exact meaning and its context here: https://doi.org/10.47757/pal.2 http

It would be somewhat lengthy to explain its meaning exactly here. You can read about its exact meaning and its context here: https://doi.org/10.47757/pal.2 https://doi.org/10.47757/pal.2 In short what it usually means (the exact meaning depends on the model under consideration) is that there is a binary operation "=", such that "x = x" is a theorem, that is evaluating "x = x" will evaluate to "true" for any object x in the mathematical universe. Furthermore, for any unary proper operator "P", and any two objects x and y of the mathematical universe, the expression "(x = y) => (P[x] => P[y])" will also evaluate to "true". Here "=>" is another binary operation called implication, which has some special properties outlined in the link. P[x] denotes the application of the operator P to the object x. Edit: Oh, forgot to add the third axiom for equality (it is actually more an axiom about "true", but uses equality): 3) A => (A = true) What this means is that for any object A of the mathematical universe, if you evaluate "A => (A = true)", you obtain the value "true".