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 2328  rab0 2927  zfnuleu 3497  dfid3 3651  reusv2lem5 3877  reusv5OLD 3882  reusv7OLD 3884  relop 4191  ruv 6262  konigthlem 6820  avril1 14765  mathbox 16527  foo3 16528  domep 17082  dffix2 17401  elfuns 17409  vecval3b 18456  elnev 21478  ipo0 21491  ifr0 21492
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