Theorem equid 1766

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 1605; see the proof of equid1 1916. See equidALT 1767 for an alternate proof.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 1598	. . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
2	1	pm2.43i 108	. . . 4 |- (-. A.x x = x -> (x = x -> A.x x = x))
3	2	alimi 1627	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax-9o 1763	. . 3 |- (A.x(x = x -> A.x x = x) -> x = x)
5	3, 4	syl 13	. 2 |- (A.x -. A.x x = x -> x = x)
6		ax-6o 1613	. 2 |- (-. A.x -. A.x x = x -> x = x)
7	5, 6	pm2.61i 192	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 1584   = wceq 1586

This theorem is referenced by:  stdpc6 1768  equcomi 1769  equveli 1812  sbid 1828  ax11eq 2018  a12lem1 2031  eubii 2046  mobii 2066  exists1 2121  vjust 2539  rab0 3101  zfnuleu 3610  dfid3 3748  reusv2lem5 3971  reusv5OLD 3976  reusv7OLD 3978  rabxfr 3989  reuhyp 3995  relop 4242  fo1st 5138  fo2nd 5139  fimax 5846  ruv 5936  alephfplem3 6229  konigthlem 6429  fsum1s 8665  fsump1s 8669  avril1 11013  symgval 11034  symggrpi 11037  mathbox 12845  foo3 12846  domep 14493  dffix2 14766  elfuns 14774  fprod1s 15416  fprodp1s 15421  vecval3b 15548  fimaxOLD 16570  elnev 17228  ipo0 17250  ifr0 17251

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-12 1598  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763

Copyright terms: Public domain