Theorem equid 1747

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.

Step	Hyp	Ref	Expression
1		a9e 1742	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
2		ax-17 1572	. . 3 ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3		ax-8 1550	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
4	3	pm2.43i 49	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
5	2, 4	exlimih 1639	. 2 ⊢ (∃𝑦 𝑦 = 𝑥 → 𝑥 = 𝑥)
6	1, 5	ax-mp 5	1 ⊢ 𝑥 = 𝑥

Syntax hints:  ∃wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1748  stdpc6  1749  equcomi  1750  equveli  1805  sbid  1820  ax16i  1904  exists1  2174  vjust  2800  vex  2802  reu6  2992  nfccdeq  3026  sbc8g  3036  dfnul3  3494  rab0  3520  int0  3936  ruv  4641  dcextest  4672  relop  4871  f1eqcocnv  5914  mpoxopoveq  6384  snexxph  7113