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

Theorem equid 1681
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 1683. See equidALT 1682 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 1583 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1465 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1563 . . . . . . 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 1597 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1441
This theorem is referenced by:  stdpc6  1684  equcomi-o  1686  equveli  1733  sbid  1749  ax11eq  1946  eubii  1964  mobii  1984  exists1  2039  vjust  2477  rab0  3093  zfnuleu  3712  dfid3  3867  reusv2lem5  4108  reusv5OLD  4113  reusv7OLD  4115  relop  4422  ruv  6803  konigthlem  7668  isppw2  18924  avril1  19387  mathbox  21574  foo3  21575  domep  22036  dffix2  22340  elfuns  22348  vecval3b  23289  mamulid  25292  elnev  25476  ipo0  25490  ifr0  25491  a12lem1  27500
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 1563  ax-9 1583  ax-4 1590
Copyright terms: Public domain