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	|- A. x x = x

Proof

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