Theorem equid 1694

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

Syntax hints:   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfequid  1695  stdpc6  1696  equcomi  1697  equveli  1752  sbid  1767  ax16i  1851  exists1  2115  vjust  2731  vex  2733  reu6  2919  nfccdeq  2953  sbc8g  2962  dfnul3  3417  rab0  3443  int0  3845  ruv  4534  dcextest  4565  relop  4761  f1eqcocnv  5770  mpoxopoveq  6219  snexxph  6927