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

Theorem equid 1719
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 1608; see the proof of equid1 1721. See equidALT 1720 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1620 . . 3 |- -. A.x -. x = x
2 hbn1 1650 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1599 . . . . . . 7 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
43pm2.43i 45 . . . . . 6 |- (-. A.x x = x -> (x = x -> A.x x = x))
54con3d 140 . . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
65pm2.43i 45 . . . 4 |- (-. A.x x = x -> -. x = x)
72, 6alrimi 1534 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 202 . 2 |- A.x x = x
98a4i 1633 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3  A.wal 1515
This theorem is referenced by:  stdpc6 1722  equveli 1762  sbid 1777  ax11eq 1969  a12lem1 1982  eubii 1997  mobii 2017  exists1 2072  vjust 2500  rab0 3085  zfnuleu 3615  dfid3 3766  reusv2lem5 3989  reusv5OLD 3994  reusv7OLD 3996  rabxfr 4007  reuhyp 4013  relop 4278  ruv 6110  alephfplem3 6479  konigthlem 6666  fsum1s 9197  fsump1s 9201  avril1 11659  symggrpi 11681  mathbox 13476  foo3 13477  domep 14051  dffix2 14321  elfuns 14329  fprod1s 15162  fprodp1s 15167  vecval3b 15301  elnev 17025  ipo0 17038  ifr0 17039
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-gen 1519  ax-12 1599  ax-9 1620  ax-4 1626
Copyright terms: Public domain