Theorem equid 1322

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 1155; see the proof of equid1 1484. See equidALT 1323 for an alternate proof.

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Step	Hyp	Ref	Expression
1		ax-12 1148	. . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
2	1	pm2.43i 78	. . . 4 |- (-. A.x x = x -> (x = x -> A.x x = x))
3	2	alimi 1176	. . 3 |- (A.x -. A.x x = x -> A.x(x = x -> A.x x = x))
4		ax-9o 1319	. . 3 |- (A.x(x = x -> A.x x = x) -> x = x)
5	3, 4	syl 12	. 2 |- (A.x -. A.x x = x -> x = x)
6		ax-6o 1162	. 2 |- (-. A.x -. A.x x = x -> x = x)
7	5, 6	pm2.61i 139	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 1134   = wceq 1136

This theorem is referenced by:  stdpc6 1324  equcomi 1325  equviniOLD 1370  sbid 1387  ax11eq 1592  a12lem1 1605  eubii 1618  mobii 1638  exists1 1699  vjust 2126  rab0 2716  zfnuleu 3257  dfid3 3402  rabxfr 3654  reuhyp 3660  relop 3924  asymref2OLD 4122  fo1st 4843  fo2nd 4844  ruv 5514  alephfplem3 5842  fsum1s 8064  fsump1s 8068  avril1 9937  symgval 9995  symggrpi 9998  mathbox 11806  foo3 11807  elsnres 13619  domep 13652  fprod1s 14401  fprodp1s 14406  vecval3b 14518  fimax 15428  elnev 16086  ipo0 16108  ifr0 16109

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-12 1148  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319

Copyright terms: Public domain