Theorem equid 1678

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

Syntax hints:  ∃wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfequid  1679  stdpc6  1680  equcomi  1681  equveli  1733  sbid  1748  ax16i  1831  exists1  2096  vjust  2690  vex  2692  reu6  2877  nfccdeq  2911  sbc8g  2920  dfnul3  3371  rab0  3396  int0  3793  ruv  4473  dcextest  4503  relop  4697  f1eqcocnv  5700  mpoxopoveq  6145  snexxph  6846