Theorem equid 1749

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

Syntax hints:  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1750  stdpc6  1751  equcomi  1752  equveli  1808  sbid  1823  ax16i  1907  exists1  2179  vjust  2816  vex  2818  reu6  3009  nfccdeq  3043  sbc8g  3053  dfnul3  3515  rab0  3541  int0  3968  ruv  4677  dcextest  4708  relop  4910  f1eqcocnv  5970  mpoxopoveq  6484  snexxph  7233