Theorem equid 1712

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 1707	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
2		ax-17 1537	. . 3 ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3		ax-8 1515	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
4	3	pm2.43i 49	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
5	2, 4	exlimih 1604	. 2 ⊢ (∃𝑦 𝑦 = 𝑥 → 𝑥 = 𝑥)
6	1, 5	ax-mp 5	1 ⊢ 𝑥 = 𝑥

Syntax hints:  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1713  stdpc6  1714  equcomi  1715  equveli  1770  sbid  1785  ax16i  1869  exists1  2138  vjust  2761  vex  2763  reu6  2950  nfccdeq  2984  sbc8g  2994  dfnul3  3450  rab0  3476  int0  3885  ruv  4583  dcextest  4614  relop  4813  f1eqcocnv  5835  mpoxopoveq  6295  snexxph  7011