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

Theorem equid 1580
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 1465; see the proof of equid1 1582. See equidALT 1581 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1480 . . 3 |- -. A.x -. x = x
2 hbn1 1511 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1456 . . . . . . 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 1385 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 177 . 2 |- A.x x = x
98a4i 1493 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1366
This theorem is referenced by:  stdpc6 1583  equveli 1623  sbid 1638  ax11eq 1830  a12lem1 1843  eubii 1858  mobii 1878  exists1 1933  vjust 2359  rab0 2941  zfnuleu 3475  dfid3 3625  reusv2lem5 3849  reusv5OLD 3854  reusv7OLD 3856  relop 4148  ruv 6044  konigthlem 6548  symggrpi 10746  avril1 12814  mathbox 14344  foo3 14345  domep 14574  dffix2 14893  elfuns 14901  vecval3b 15948  elnev 17472  ipo0 17485  ifr0 17486
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-gen 1370  ax-12 1456  ax-9 1480  ax-4 1486
Copyright terms: Public domain