MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equid Unicode version

Theorem equid 1685
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 1533; see the proof of equid1 1687. See equidALT 1686 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 1587 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1469 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1567 . . . . . . 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 1464 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1601 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1445
This theorem is referenced by:  stdpc6  1688  equcomi-o  1690  equveli  1737  sbid  1753  ax11eq  1950  eubii  1968  mobii  1988  exists1  2043  vjust  2481  rab0  3097  zfnuleu  3716  dfid3  3871  reusv2lem5  4112  reusv5OLD  4117  reusv7OLD  4119  relop  4426  ruv  6807  konigthlem  7672  isppw2  18928  avril1  19391  mathbox  21578  foo3  21579  domep  22040  dffix2  22344  elfuns  22352  vecval3b  23294  mamulid  25330  elnev  25514  ipo0  25528  ifr0  25529  a12lem1  27535
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-gen 1449  ax-12o 1567  ax-9 1587  ax-4 1594
  Copyright terms: Public domain W3C validator