Theorem equid 1159

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 1004; see the proof of equid1 1305. See equidALT 1160 for an alternate proof.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 1001	. . . . 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 1025	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax-9o 1156	. . 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 1011	. 2 |- (-. A.x -. A.x x = x -> x = x)
7	5, 6	pm2.61i 124	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 987   = wceq 989

This theorem is referenced by:  stdpc6 1161  equcomi 1162  equvini 1202  sbid 1218  ax11eq 1400  a12lem1 1413  eubii 1424  mobii 1442  exists1 1496  zfnuleu 2777  dfid3 2910  relop 3362  asymref2 3529  fo1st 4147  fo2nd 4148  ruv 4735  alephfplem3 5039  fsum1s 7200  fsump1s 7204  avril1 9035  sandbox 10626  foo3 10627  symgval 10663  symggrpi 10666

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 996  ax-12 1001  ax-4 1006  ax-5o 1008  ax-6o 1011  ax-9o 1156

Copyright terms: Public domain