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 2919  zfnuleu 3460  dfid3 3612  reusv2lem5 3836  reusv5OLD 3841  reusv7OLD 3843  relop 4135  ruv 6051  konigthlem 6554  symggrpi 10822  avril1 12978  mathbox 14508  foo3 14509  domep 14738  dffix2 15057  elfuns 15065  vecval3b 16112  elnev 18182  ipo0 18195  ifr0 18196
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