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

Theorem equid 1559
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 1444; see the proof of equid1 1561. See equidALT 1560 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1459 . . 3 |- -. A.x -. x = x
2 hbn1 1490 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1435 . . . . . . 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 1363 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 168 . 2 |- A.x x = x
98a4i 1472 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1344
This theorem is referenced by:  stdpc6 1562  equveli 1602  sbid 1617  ax11eq 1809  a12lem1 1822  eubii 1837  mobii 1857  exists1 1912  vjust 2338  rab0 2920  zfnuleu 3456  dfid3 3608  reusv2lem5 3832  reusv5OLD 3837  reusv7OLD 3839  relop 4131  ruv 6028  konigthlem 6532  symggrpi 10787  avril1 12943  mathbox 14473  foo3 14474  domep 14703  dffix2 15022  elfuns 15030  vecval3b 16077  elnev 17601  ipo0 17614  ifr0 17615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-gen 1348  ax-12 1435  ax-9 1459  ax-4 1465
Copyright terms: Public domain