Theorem equid 1677

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

Syntax hints:   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfequid  1678  stdpc6  1679  equcomi  1680  equveli  1732  sbid  1747  ax16i  1830  exists1  2095  vjust  2687  vex  2689  reu6  2873  nfccdeq  2907  sbc8g  2916  dfnul3  3366  rab0  3391  int0  3785  ruv  4465  dcextest  4495  relop  4689  f1eqcocnv  5692  mpoxopoveq  6137  snexxph  6838