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

Theorem equid 1588
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 1473; see the proof of equid1 1590. See equidALT 1589 for an alternate proof.
Assertion
Ref Expression
equid |- x = x

Proof of Theorem equid
StepHypRef Expression
1 ax-9 1488 . . 3 |- -. A.x -. x = x
2 hbn1 1519 . . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3 ax-12 1464 . . . . . . 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 125 . . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
65pm2.43i 45 . . . 4 |- (-. A.x x = x -> -. x = x)
72, 6alrimi 1394 . . 3 |- (-. A.x x = x -> A.x -. x = x)
81, 7mt3 182 . 2 |- A.x x = x
98a4i 1501 1 |- x = x
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1375
This theorem is referenced by:  stdpc6 1591  equveli 1631  sbid 1646  ax11eq 1838  a12lem1 1851  eubii 1866  mobii 1886  exists1 1941  vjust 2367  rab0 2947  zfnuleu 3481  dfid3 3631  reusv2lem5 3855  reusv5OLD 3860  reusv7OLD 3862  rabxfr 3878  reuhyp 3884  relop 4152  ruv 6045  alephfplem3 6371  konigthlem 6558  symggrpi 10647  avril1 12560  mathbox 14090  foo3 14091  domep 14325  dffix2 14644  elfuns 14652  vecval3b 15705  elnev 17266  ipo0 17279  ifr0 17280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-gen 1379  ax-12 1464  ax-9 1488  ax-4 1494
Copyright terms: Public domain