Theorem equid 1113

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 1190; see the proof of equid1 1253.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 1104	. . . . 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 968	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax9 1110	. . 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-6 953	. 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 950   = wceq 1099

This theorem is referenced by:  stdpc6 1114  equcomi 1115  equvini 1151  sbid 1167  ax11eq 1340  a12lem1 1353  eubii 1364  mobii 1382  exists1 1434  zfnuleu 2675  dfid3 2799  fo1st 4029  fo2nd 4030  2nd2val 4034  alephfplem3 4821  fsum1s 6898  fsump1s 6902  ser1f0 7057  sandbox 8636  symgval 8670  symggrpi 8673  avril1 8964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain