Theorem equid 1586

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 y. 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	⊢ x = x

Proof of Theorem equid

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		a9e 1583	. 2 ⊢ ∃y y = x
2		ax-17 1416	. . 3 ⊢ (x = x → ∀y x = x)
3		ax-8 1392	. . . 4 ⊢ (y = x → (y = x → x = x))
4	3	pm2.43i 43	. . 3 ⊢ (y = x → x = x)
5	2, 4	exlimih 1481	. 2 ⊢ (∃y y = x → x = x)
6	1, 5	ax-mp 7	1 ⊢ x = x

Syntax hints:  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-8 1392  ax-17 1416  ax-i9 1420

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfequid  1587  stdpc6  1588  equcomi  1589  equveli  1639  sbid  1654  ax16i  1735  exists1  1993  vjust  2552  vex  2554  reu6  2724  nfccdeq  2756  sbc8g  2765  dfnul3  3221  rab0  3240  int0  3620  ruv  4228  relop  4429  f1eqcocnv  5374  mpt2xopoveq  5796