Theorem equid 1658

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

Syntax hints:   E.wex 1449

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1406  ax-ie2 1451  ax-8 1463  ax-17 1487  ax-i9 1491

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfequid  1659  stdpc6  1660  equcomi  1661  equveli  1713  sbid  1728  ax16i  1810  exists1  2069  vjust  2656  vex  2658  reu6  2840  nfccdeq  2874  sbc8g  2883  dfnul3  3330  rab0  3355  int0  3749  ruv  4423  dcextest  4453  relop  4647  f1eqcocnv  5644  mpoxopoveq  6089  snexxph  6788