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

Theorem equid1 2235
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 1626; see the proof of equid 1688. See equid1ALT 2253 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
equid1  |-  x  =  x

Proof of Theorem equid1
StepHypRef Expression
1 ax-5o 2213 . . . 4  |-  ( A. x ( A. x  -.  A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
)  ->  ( A. x  -.  A. x  x  =  x  ->  A. x
( x  =  x  ->  A. x  x  =  x ) ) )
2 ax-4 2212 . . . . 5  |-  ( A. x  -.  A. x  x  =  x  ->  -.  A. x  x  =  x )
3 ax-12o 2219 . . . . 5  |-  ( -. 
A. x  x  =  x  ->  ( -.  A. x  x  =  x  ->  ( x  =  x  ->  A. x  x  =  x )
) )
42, 2, 3sylc 58 . . . 4  |-  ( A. x  -.  A. x  x  =  x  ->  (
x  =  x  ->  A. x  x  =  x ) )
51, 4mpg 1557 . . 3  |-  ( A. x  -.  A. x  x  =  x  ->  A. x
( x  =  x  ->  A. x  x  =  x ) )
6 ax-9o 2215 . . 3  |-  ( A. x ( x  =  x  ->  A. x  x  =  x )  ->  x  =  x )
75, 6syl 16 . 2  |-  ( A. x  -.  A. x  x  =  x  ->  x  =  x )
8 ax-6o 2214 . 2  |-  ( -. 
A. x  -.  A. x  x  =  x  ->  x  =  x )
97, 8pm2.61i 158 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1549
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-4 2212  ax-5o 2213  ax-6o 2214  ax-9o 2215  ax-12o 2219
  Copyright terms: Public domain W3C validator