HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem equid 1565
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 1450; see the proof of equid1 1567. See equidALT 1566 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1465 . . 3 |- -. A.x -. x = x
2 hbn1 1496 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1441 . . . . . . 7 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
43pm2.43i 42 . . . . . 6 |- (-. A.x x = x -> (x = x -> A.x x = x))
54con3d 122 . . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
65pm2.43i 42 . . . 4 |- (-. A.x x = x -> -. x = x)
72, 6alrimi 1369 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 168 . 2 |- A.x x = x
98a4i 1478 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1350
This theorem is referenced by:  stdpc6 1568  equveli 1608  sbid 1623  ax11eq 1815  a12lem1 1828  eubii 1843  mobii 1863  exists1 1918  vjust 2344  rab0 2926  zfnuleu 3464  dfid3 3616  reusv2lem5 3840  reusv5OLD 3845  reusv7OLD 3847  relop 4139  ruv 6037  konigthlem 6540  symggrpi 10798  avril1 12954  mathbox 14484  foo3 14485  domep 14714  dffix2 15033  elfuns 15041  vecval3b 16088  elnev 17612  ipo0 17625  ifr0 17626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-gen 1354  ax-12 1441  ax-9 1465  ax-4 1471
Copyright terms: Public domain