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

Theorem equid 1587
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 1473; see the proof of equid1 1589. See equidALT 1588 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1488 . . 3 |- -. A.x -. x = x
2 hbn1 1518 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1464 . . . . . . 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 125 . . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
65pm2.43i 45 . . . 4 |- (-. A.x x = x -> -. x = x)
72, 6alrimi 1394 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 182 . 2 |- A.x x = x
98a4i 1501 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1375
This theorem is referenced by:  stdpc6 1590  equveli 1630  sbid 1645  ax11eq 1837  a12lem1 1850  eubii 1865  mobii 1885  exists1 1940  vjust 2366  rab0 2946  zfnuleu 3478  dfid3 3628  reusv2lem5 3852  reusv5OLD 3857  reusv7OLD 3859  rabxfr 3870  reuhyp 3876  relop 4144  ruv 6006  alephfplem3 6332  konigthlem 6519  symggrpi 10611  avril1 11954  mathbox 13484  foo3 13485  domep 14002  dffix2 14321  elfuns 14329  vecval3b 15386  elnev 16953  ipo0 16966  ifr0 16967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-gen 1379  ax-12 1464  ax-9 1488  ax-4 1494
Copyright terms: Public domain