Theorem equid 1128

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 973; see the proof of equid1 1271.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 970	. . . . 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 994	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax-9o 1125	. . 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 980	. 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 956   = wceq 958

This theorem is referenced by:  stdpc6 1129  equcomi 1130  equvini 1170  sbid 1186  ax11eq 1365  a12lem1 1378  eubii 1389  mobii 1407  exists1 1460  zfnuleu 2712  dfid3 2842  relop 3281  asymref2 3446  fo1st 4097  fo2nd 4098  alephfplem3 4909  fsum1s 7009  fsump1s 7013  avril1 8779  sandbox 10364  symgval 10398  symggrpi 10401

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

Copyright terms: Public domain