HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem equid 1678
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 1527; see the proof of equid1 1680. See equidALT 1679 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 1580 . . 3  |-  -.  A. x  -.  x  =  x
2 hbn1 1463 . . . 4  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  A. x  x  =  x )
3 ax-12o 1560 . . . . . . 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 1458 . . 3  |-  ( -. 
A. x  x  =  x  ->  A. x  -.  x  =  x
)
81, 7mt3 169 . 2  |-  A. x  x  =  x
98a4i 1594 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1439
This theorem is referenced by:  stdpc6  1681  equcomi-o  1683  equveli  1730  sbid  1746  ax11eq  1943  eubii  1961  mobii  1981  exists1  2036  vjust  2474  rab0  3090  zfnuleu  3704  dfid3  3859  reusv2lem5  4100  reusv5OLD  4105  reusv7OLD  4107  relop  4414  ruv  6793  konigthlem  7658  isppw2  18301  avril1  18658  mathbox  20845  foo3  20846  domep  21311  dffix2  21615  elfuns  21623  vecval3b  22564  mamulid  24568  elnev  24753  ipo0  24767  ifr0  24768  a12lem1  26773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-gen 1443  ax-12o 1560  ax-9 1580  ax-4 1587
Copyright terms: Public domain