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

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

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1444 . . 3
2 hbn1 1475 . . . 4
3 ax-12 1420 . . . . . . 7
43pm2.43i 42 . . . . . 6
54con3d 122 . . . . 5
65pm2.43i 42 . . . 4
72, 6alrimi 1348 . . 3
81, 7mt3 168 . 2
98a4i 1457 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1329
This theorem is referenced by:  stdpc6 1547  equveli 1587  sbid 1602  ax11eq 1794  a12lem1 1807  eubii 1822  mobii 1842  exists1 1897  vjust 2323  rab0 2918  zfnuleu 3460  dfid3 3612  reusv2lem5 3838  reusv5OLD 3843  reusv7OLD 3845  relop 4147  ruv 6127  konigthlem 6656  avril1 13582  mathbox 15118  foo3 15119  domep 15656  dffix2 15975  elfuns 15983  vecval3b 17045  elnev 19459  ipo0 19472  ifr0 19473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-gen 1333  ax-12 1420  ax-9 1444  ax-4 1450
Copyright terms: Public domain