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

Theorem equid 1697
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 1542; see the proof of equid1 1699. See equidALT 1698 for an alternate proof.
Assertion
Ref Expression
equid

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1563 . . 3
2 hbn1 1469 . . . 4
3 ax-12 1537 . . . . . . 7
43pm2.43i 43 . . . . . 6
54con3d 123 . . . . 5
65pm2.43i 43 . . . 4
72, 6alrimi 1464 . . 3
81, 7mt3 169 . 2
98a4i 1612 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1445
This theorem is referenced by:  stdpc6  1700  equveli  1748  sbid  1763  ax11eq  1961  a12lem1  1974  eubii  1989  mobii  2009  exists1  2064  vjust  2501  rab0  3105  zfnuleu  3693  dfid3  3849  reusv2lem5  4090  reusv5OLD  4095  reusv7OLD  4097  relop  4408  ruv  6727  konigthlem  7565  avril1  16171  mathbox  18361  foo3  18362  domep  18833  dffix2  19141  elfuns  19149  vecval3b  20092  elnev  22314  ipo0  22328  ifr0  22329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-gen 1449  ax-12 1537  ax-9 1563  ax-4 1605
Copyright terms: Public domain