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

Theorem equid 1818
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 1628; see the proof of equid1 1820. See equidALT 1819 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 1684 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1564 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1664 . . . . . . 7  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
) )
43pm2.43i 45 . . . . . 6  |-  ( -. 
A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
)
54con3d 127 . . . . 5  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  -.  x  =  x ) )
65pm2.43i 45 . . . 4  |-  ( -. 
A. x  x  =  x  ->  -.  x  =  x )
72, 6alrimih 1553 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 173 . 2  |-  A. x  x  =  x
98a4i 1699 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1532
This theorem is referenced by:  stdpc6  1821  equcomi-o  1823  equveli  1881  sbid  1896  ax11eq  2108  exists1  2205  vjust  2741  nfccdeq  2933  sbc8g  2942  rab0  3417  dfid3  4247  reusv5OLD  4481  reusv7OLD  4483  relop  4787  fv2  5419  fsplit  6122  ruv  7247  konigthlem  8123  alexsubALTlem3  17670  isppw2  20280  avril1  20761  mathbox  22947  foo3  22948  domep  23483  dffix2  23786  elfuns  23794  vecval3b  24784  mamulid  26790  elnev  26971  ipo0  26985  ifr0  26986  a12lem1  28260
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-12o 1664  ax-9 1684  ax-4 1692
  Copyright terms: Public domain W3C validator