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  1807  sbid  1822  ax16i  1906  exists1  2176  vjust  2804  vex  2806  reu6  2996  nfccdeq  3030  sbc8g  3040  dfnul3  3499  rab0  3525  int0  3947  ruv  4654  dcextest  4685  relop  4886  f1eqcocnv  5942  mpoxopoveq  6449  snexxph  7192