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

Theorem equid 1698
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 1545; see the proof of equid1 1700. See equidALT 1699 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 1598 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1474 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1578 . . . . . . 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 1469 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1613 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1450
This theorem is referenced by:  stdpc6  1701  equcomi-o  1703  equveli  1750  sbid  1766  ax11eq  1963  eubii  1981  mobii  2001  exists1  2056  vjust  2493  rab0  3108  zfnuleu  3720  dfid3  3875  reusv2lem5  4116  reusv5OLD  4121  reusv7OLD  4123  relop  4433  ruv  6777  konigthlem  7642  avril1  18060  mathbox  20243  foo3  20244  domep  20739  dffix2  21045  elfuns  21053  vecval3b  22000  mamulid  23986  elnev  24201  ipo0  24215  ifr0  24216  a12lem1  26222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-gen 1454  ax-12o 1578  ax-9 1598  ax-4 1606
Copyright terms: Public domain