This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ∀ 𝑥 𝑥 = 𝑥

Proof

Step	Hyp	Ref	Expression
1		equid	⊢ 𝑥 = 𝑥
2	1	ax-gen	⊢ ∀ 𝑥 𝑥 = 𝑥