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

Theorem equid 1556
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 1441; see the proof of equid1 1558. See equidALT 1557 for an alternate proof.
Assertion
Ref Expression
equid

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1456 . . 3
2 hbn1 1487 . . . 4
3 ax-12 1432 . . . . . . 7
43pm2.43i 42 . . . . . 6
54con3d 122 . . . . 5
65pm2.43i 42 . . . 4
72, 6alrimi 1360 . . 3
81, 7mt3 168 . 2
98a4i 1469 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1341
This theorem is referenced by:  stdpc6 1559  equveli 1599  sbid 1614  ax11eq 1806  a12lem1 1819  eubii 1834  mobii 1854  exists1 1909  vjust 2336  rab0 2923  zfnuleu 3464  dfid3 3616  reusv2lem5 3840  reusv5OLD 3845  reusv7OLD 3847  relop 4139  ruv 6067  konigthlem 6570  symggrpi 11093  avril1 13241  mathbox 14777  foo3 14778  domep 15131  dffix2 15450  elfuns 15458  vecval3b 16522  elnev 18807  ipo0 18820  ifr0 18821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-gen 1345  ax-12 1432  ax-9 1456  ax-4 1462
Copyright terms: Public domain