Theorem eqid 810

Description: Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. 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 is not as obvious as you might think.) This proof uses only axioms without distinct variable conditions and thus involves no dummy variables. A shorter proof, similar to Tarki's, is possible if we make use of ax-17 925; see the proof of x = x on the Metamath Solitaire page.

Assertion

Ref	Expression
eqid	⊢ x = x

Proof of Theorem eqid

Step	Hyp	Ref	Expression
1		ax-12 802	. . . . 5 ⊢ (¬ ∀x x = x → (¬ ∀x x = x → (x = x → ∀x x = x)))
2	1	pm2.43i 58	. . . 4 ⊢ (¬ ∀x x = x → (x = x → ∀x x = x))
3	2	19.20i 691	. . 3 ⊢ (∀x ¬ ∀x x = x → ∀x(x = x → ∀x x = x))
4		ax9 807	. . 3 ⊢ (∀x(x = x → ∀x x = x) → x = x)
5	3, 4	syl 12	. 2 ⊢ (∀x ¬ ∀x x = x → x = x)
6		ax-6 675	. 2 ⊢ (¬ ∀x ¬ ∀x x = x → x = x)
7	5, 6	pm2.61i 110	1 ⊢ x = x

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672   = weq 797

This theorem is referenced by:  eqcom 811  eqvin.l1 851  sbid 868  bieu 1014  bimo 1031  exists1 1072  sbcgf 1469  fo1st 3094  fo2nd 3095

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org