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

Theorem equid 1692
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 1540; see the proof of equid1 1694. See equidALT 1693 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 1594 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1475 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1574 . . . . . . 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 1470 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1608 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1451
This theorem is referenced by:  stdpc6  1695  equcomi-o  1697  equveli  1744  sbid  1760  ax11eq  1957  eubii  1975  mobii  1995  exists1  2050  vjust  2513  rab0  3130  zfnuleu  3750  dfid3  3905  reusv2lem5  4146  reusv5OLD  4151  reusv7OLD  4153  relop  4460  fv2  5084  fsplit  5752  ruv  6841  konigthlem  7706  alexsubALTlem3  16485  isppw2  18962  avril1  19425  mathbox  21612  foo3  21613  domep  22074  dffix2  22378  elfuns  22386  vecval3b  23338  mamulid  25393  elnev  25575  ipo0  25589  ifr0  25590  a12lem1  26533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-gen 1455  ax-12o 1574  ax-9 1594  ax-4 1601
  Copyright terms: Public domain W3C validator