Description: One of the two equality axioms of standard predicate calculus, called
reflexivity of equality. (The other one is stdpc7 .) Axiom 6 of
Mendelson p. 95. Mendelson doesn't say why he prepended the redundant
quantifier, but it was probably to be compatible with free logic (which is
valid in the empty domain). (Contributed by NM, 16-Feb-2005)