Metamath Proof Explorer


Theorem stdpc6

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)

Ref Expression
Assertion stdpc6 x x = x

Proof

Step Hyp Ref Expression
1 equid x = x
2 1 ax-gen x x = x