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

Theorem equid 1677
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 1526; see the proof of equid1 1679. See equidALT 1678 for an alternate proof. (Contributed by NM, 30-Nov-2008.)
Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1579 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1462 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1559 . . . . . . 7  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
) )
43pm2.43i 43 . . . . . 6  |-  ( -. 
A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
)
54con3d 123 . . . . 5  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  -.  x  =  x ) )
65pm2.43i 43 . . . 4  |-  ( -. 
A. x  x  =  x  ->  -.  x  =  x )
72, 6alrimi 1457 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1593 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1438
This theorem is referenced by:  stdpc6  1680  equcomi-o  1682  equveli  1729  sbid  1745  ax11eq  1942  eubii  1960  mobii  1980  exists1  2035  vjust  2473  rab0  3089  zfnuleu  3703  dfid3  3858  reusv2lem5  4099  reusv5OLD  4104  reusv7OLD  4106  relop  4413  ruv  6791  konigthlem  7656  avril1  18418  mathbox  20605  foo3  20606  domep  21090  dffix2  21394  elfuns  21402  vecval3b  22342  mamulid  24343  elnev  24528  ipo0  24542  ifr0  24543  a12lem1  26548
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-gen 1442  ax-12o 1559  ax-9 1579  ax-4 1586
Copyright terms: Public domain