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

Theorem equid 1657
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 1659. See equidALT 1658 for an alternate proof.
Assertion
Ref Expression
equid

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1557 . . 3
2 hbn1 1588 . . . 4
3 ax-12 1533 . . . . . . 7
43pm2.43i 43 . . . . . 6
54con3d 123 . . . . 5
65pm2.43i 43 . . . 4
72, 6alrimi 1461 . . 3
81, 7mt3 169 . 2
98a4i 1570 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1442
This theorem is referenced by:  stdpc6 1660  equveli 1700  sbid 1715  ax11eq 1907  a12lem1 1920  eubii 1935  mobii 1955  exists1 2010  vjust 2441  rab0 3045  zfnuleu 3632  dfid3 3788  reusv2lem5 4014  reusv5OLD 4019  reusv7OLD 4021  relop 4329  ruv 6580  konigthlem 7410  avril1 15865  mathbox 18073  foo3 18074  domep 18528  dffix2 18846  elfuns 18854  vecval3b 19798  elnev 22016  ipo0 22029  ifr0 22030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-gen 1446  ax-12 1533  ax-9 1557  ax-4 1563
Copyright terms: Public domain