Theorem equid1 39693

Description: Proof of equid 2042 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 1940; see the proof of equid 2042. See equid1ALT 39719 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 39678	. . . 4 ⊢ (∀𝑥(∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) → (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
2		ax-c5 39677	. . . . 5 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ¬ ∀𝑥 𝑥 = 𝑥)
3		ax-c9 39684	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑥 → (¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)))
4	2, 2, 3	sylc 66	. . . 4 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → (𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
5	1, 4	mpg 1827	. . 3 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
6		ax-c10 39680	. . 3 ⊢ (∀𝑥(𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) → 𝑥 = 𝑥)
7	5, 6	syl 18	. 2 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥)
8		ax-c7 39679	. 2 ⊢ (¬ ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑥 → 𝑥 = 𝑥)
9	7, 8	pm2.61i 184	1 ⊢ 𝑥 = 𝑥

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-c5 39677  ax-c4 39678  ax-c7 39679  ax-c10 39680  ax-c9 39684

This theorem is referenced by:  equcomi1  39694