Theorem equid 1715

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

Syntax hints:   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1716  stdpc6  1717  equcomi  1718  equveli  1773  sbid  1788  ax16i  1872  exists1  2141  vjust  2764  vex  2766  reu6  2953  nfccdeq  2987  sbc8g  2997  dfnul3  3453  rab0  3479  int0  3888  ruv  4586  dcextest  4617  relop  4816  f1eqcocnv  5838  mpoxopoveq  6298  snexxph  7016