Theorem equid 1126

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 971; see the proof of equid1 1269.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 968	. . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
2	1	pm2.43i 64	. . . 4 |- (-. A.x x = x -> (x = x -> A.x x = x))
3	2	19.20i 992	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax-9o 1123	. . 3 |- (A.x(x = x -> A.x x = x) -> x = x)
5	3, 4	syl 10	. 2 |- (A.x -. A.x x = x -> x = x)
6		ax-6o 978	. 2 |- (-. A.x -. A.x x = x -> x = x)
7	5, 6	pm2.61i 126	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  stdpc6 1127  equcomi 1128  equvini 1168  sbid 1184  ax11eq 1363  a12lem1 1376  eubii 1387  mobii 1405  exists1 1457  zfnuleu 2707  dfid3 2836  relop 3275  asymref2 3440  fo1st 4091  fo2nd 4092  alephfplem3 4890  fsum1s 6994  fsump1s 6998  avril1 8769  sandbox 10354  symgval 10388  symggrpi 10391

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

Copyright terms: Public domain