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 3465  dfid3 3617  reusv2lem5 3841  reusv5OLD 3846  reusv7OLD 3848  relop 4140  ruv 6052  konigthlem 6555  symggrpi 10820  avril1 12976  mathbox 14506  foo3 14507  domep 14736  dffix2 15055  elfuns 15063  vecval3b 16110  elnev 17634  ipo0 17647  ifr0 17648
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