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

Theorem equid 1680
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 1529; see the proof of equid1 1682. See equidALT 1681 for an alternate proof. (Contributed by NM, 30-Nov-2008.) (Proof modification is discouraged.)
Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1582 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1465 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1562 . . . . . . 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 1460 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1596 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1441
This theorem is referenced by:  stdpc6  1683  equcomi-o  1685  equveli  1732  sbid  1748  ax11eq  1945  eubii  1963  mobii  1983  exists1  2038  vjust  2476  rab0  3092  zfnuleu  3706  dfid3  3861  reusv2lem5  4102  reusv5OLD  4107  reusv7OLD  4109  relop  4416  ruv  6797  konigthlem  7662  isppw2  18907  avril1  19368  mathbox  21555  foo3  21556  domep  22019  dffix2  22323  elfuns  22331  vecval3b  23272  mamulid  25275  elnev  25459  ipo0  25473  ifr0  25474  a12lem1  27479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-gen 1445  ax-12o 1562  ax-9 1582  ax-4 1589
Copyright terms: Public domain