Theorem equid1

Description: Proof of equid from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 ; see the proof of equid . See equid1ALT for an alternate proof. (Contributed by NM, 10-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equid1	⊢ 𝑥 = 𝑥

Proof

Step	Hyp	Ref	Expression
1		ax-c4	⊢ ( ∀ 𝑥 ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) ) → ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) ) )
2		ax-c5	⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → ¬ ∀ 𝑥 𝑥 = 𝑥 )
3		ax-c9	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑥 → ( ¬ ∀ 𝑥 𝑥 = 𝑥 → ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) ) )
4	2 2 3	sylc	⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) )
5	1 4	mpg	⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) )
6		ax-c10	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) → 𝑥 = 𝑥 )
7	5 6	syl	⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥 )
8		ax-c7	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥 )
9	7 8	pm2.61i	⊢ 𝑥 = 𝑥