ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  equid GIF version

Theorem equid 1660
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.

This proof is similar to Tarski's and makes use of a dummy variable 𝑦. It also works in intuitionistic logic, unlike some other possible ways of proving this theorem. (Contributed by NM, 1-Apr-2005.)

Assertion
Ref Expression
equid 𝑥 = 𝑥

Proof of Theorem equid
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 a9e 1657 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1489 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1465 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 49 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1555 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 5 1 𝑥 = 𝑥
Colors of variables: wff set class
Syntax hints:  wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nfequid  1661  stdpc6  1662  equcomi  1663  equveli  1715  sbid  1730  ax16i  1812  exists1  2071  vjust  2659  vex  2661  reu6  2844  nfccdeq  2878  sbc8g  2887  dfnul3  3334  rab0  3359  int0  3753  ruv  4433  dcextest  4463  relop  4657  f1eqcocnv  5658  mpoxopoveq  6103  snexxph  6804
  Copyright terms: Public domain W3C validator