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

Theorem equid 1807
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 1617; see the proof of equid1 1809. See equidALT 1808 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 1673 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1553 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1653 . . . . . . 7  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
) )
43pm2.43i 44 . . . . . 6  |-  ( -. 
A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
)
54con3d 124 . . . . 5  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  -.  x  =  x ) )
65pm2.43i 44 . . . 4  |-  ( -. 
A. x  x  =  x  ->  -.  x  =  x )
72, 6alrimih 1542 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 170 . 2  |-  A. x  x  =  x
98a4i 1688 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 4    -> wi 5   A.wal 1521
This theorem is referenced by:  stdpc6  1810  equcomi-o  1812  equveli  1869  sbid  1884  ax11eq  2093  exists1  2190  vjust  2713  nfccdeq  2904  sbc8g  2911  rab0  3362  dfid3  4182  reusv5OLD  4414  reusv7OLD  4416  relop  4720  fv2  5348  fsplit  6049  ruv  7172  konigthlem  8044  alexsubALTlem3  17421  isppw2  20003  avril1  20467  mathbox  22653  foo3  22654  domep  23123  dffix2  23426  elfuns  23434  vecval3b  24424  mamulid  26430  elnev  26611  ipo0  26625  ifr0  26626  a12lem1  27566
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-gen 1525  ax-12o 1653  ax-9 1673  ax-4 1681
  Copyright terms: Public domain W3C validator