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

Theorem equid 1545
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 1430; see the proof of equid1 1547. See equidALT 1546 for an alternate proof.
Assertion
Ref Expression
equid

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1445 . . 3
2 hbn1 1476 . . . 4
3 ax-12 1421 . . . . . . 7
43pm2.43i 43 . . . . . 6
54con3d 123 . . . . 5
65pm2.43i 43 . . . 4
72, 6alrimi 1349 . . 3
81, 7mt3 169 . 2
98a4i 1458 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1330
This theorem is referenced by:  stdpc6 1548  equveli 1588  sbid 1603  ax11eq 1795  a12lem1 1808  eubii 1823  mobii 1843  exists1 1898  vjust 2325  rab0 2922  zfnuleu 3472  dfid3 3624  reusv2lem5 3850  reusv5OLD 3855  reusv7OLD 3857  relop 4162  ruv 6190  konigthlem 6719  avril1 13772  mathbox 15318  foo3 15319  domep 16007  dffix2 16326  elfuns 16334  vecval3b 17386  elnev 20074  ipo0 20087  ifr0 20088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-gen 1334  ax-12 1421  ax-9 1445  ax-4 1451
Copyright terms: Public domain