Theorem equid1 37434

Description: Proof of equid 2015 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 1913; see the proof of equid 2015. See equid1ALT 37460 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
equid1	⊢ 𝑥 = 𝑥

Proof of Theorem equid1

Step	Hyp	Ref	Expression
1		ax-c4 37419	. . . 4 ⊢ (∀𝑥(∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) → (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
2		ax-c5 37418	. . . . 5 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ¬ ∀𝑥 𝑥 = 𝑥)
3		ax-c9 37425	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑥 → (¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
4	2, 2, 3	sylc 65	. . . 4 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
5	1, 4	mpg 1799	. . 3 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
6		ax-c10 37421	. . 3 ⊢ (∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → 𝑥 = 𝑥)
7	5, 6	syl 17	. 2 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥)
8		ax-c7 37420	. 2 ⊢ (¬ ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥)
9	7, 8	pm2.61i 182	1 ⊢ 𝑥 = 𝑥

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-c5 37418  ax-c4 37419  ax-c7 37420  ax-c10 37421  ax-c9 37425

This theorem is referenced by:  equcomi1  37435