Theorem equid 1724

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

Syntax hints:   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1725  stdpc6  1726  equcomi  1727  equveli  1782  sbid  1797  ax16i  1881  exists1  2150  vjust  2773  vex  2775  reu6  2962  nfccdeq  2996  sbc8g  3006  dfnul3  3463  rab0  3489  int0  3899  ruv  4598  dcextest  4629  relop  4828  f1eqcocnv  5860  mpoxopoveq  6326  snexxph  7052