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 2327  rab0 2924  zfnuleu 3485  dfid3 3638  reusv2lem5 3864  reusv5OLD 3869  reusv7OLD 3871  relop 4178  ruv 6229  konigthlem 6761  avril1 14464  mathbox 16010  foo3 16011  domep 16768  dffix2 17087  elfuns 17095  vecval3b 18142  elnev 20780  ipo0 20793  ifr0 20794
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