Theorem equid 1122

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, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and thus requires no dummy variables. A simpler proof, similar to Tarki's, is possible if we make use of ax-17 968; see the proof of equid1 1264.

Assertion

Ref	Expression
equid	⊢ x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 965	. . . . 5 ⊢ (¬ ∀x x = x → (¬ ∀x x = x → (x = x → ∀x x = x)))
2	1	pm2.43i 64	. . . 4 ⊢ (¬ ∀x x = x → (x = x → ∀x x = x))
3	2	19.20i 989	. . 3 ⊢ (∀x ¬ ∀x x = x → ∀x(x = x → ∀x x = x))
4		ax-9o 1119	. . 3 ⊢ (∀x(x = x → ∀x x = x) → x = x)
5	3, 4	syl 10	. 2 ⊢ (∀x ¬ ∀x x = x → x = x)
6		ax-6o 975	. 2 ⊢ (¬ ∀x ¬ ∀x x = x → x = x)
7	5, 6	pm2.61i 126	1 ⊢ x = x

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 951   = wceq 953

This theorem is referenced by:  stdpc6 1123  equcomi 1124  equvini 1164  sbid 1180  ax11eq 1356  a12lem1 1369  eubii 1380  mobii 1398  exists1 1450  zfnuleu 2697  dfid3 2826  relop 3265  asymref2 3424  asymref2OLD 3426  fo1st 4075  fo2nd 4076  2nd2val 4080  alephfplem3 4870  fsum1s 6947  fsump1s 6951  ser1f0 7106  avril1 8723  sandbox 10274  symgval 10308  symggrpiOLD 10311  symggrpi 10313

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

Copyright terms: Public domain