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

Theorem equid 1589
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 1586 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1419 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1395 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 43 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1484 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 7 1 𝑥 = 𝑥
Colors of variables: wff set class
Syntax hints:  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1338  ax-ie2 1383  ax-8 1395  ax-17 1419  ax-i9 1423
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfequid  1590  stdpc6  1591  equcomi  1592  equveli  1642  sbid  1657  ax16i  1738  exists1  1996  vjust  2555  vex  2557  reu6  2727  nfccdeq  2759  sbc8g  2768  dfnul3  3224  rab0  3243  int0  3626  ruv  4244  relop  4449  f1eqcocnv  5394  mpt2xopoveq  5818
  Copyright terms: Public domain W3C validator