Theorem equid 1701

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 1696	. 2 |- E. y y = x
2		ax-17 1526	. . 3 |- ( x = x -> A. y x = x )
3		ax-8 1504	. . . 4 |- ( y = x -> ( y = x -> x = x ) )
4	3	pm2.43i 49	. . 3 |- ( y = x -> x = x )
5	2, 4	exlimih 1593	. 2 |- ( E. y y = x -> x = x )
6	1, 5	ax-mp 5	1 |- x = x

Syntax hints:   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1702  stdpc6  1703  equcomi  1704  equveli  1759  sbid  1774  ax16i  1858  exists1  2122  vjust  2739  vex  2741  reu6  2927  nfccdeq  2961  sbc8g  2971  dfnul3  3426  rab0  3452  int0  3859  ruv  4550  dcextest  4581  relop  4778  f1eqcocnv  5792  mpoxopoveq  6241  snexxph  6949