Theorem equid 1629

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 1626	. 2 |- E. y y = x
2		ax-17 1459	. . 3 |- ( x = x -> A. y x = x )
3		ax-8 1435	. . . 4 |- ( y = x -> ( y = x -> x = x ) )
4	3	pm2.43i 48	. . 3 |- ( y = x -> x = x )
5	2, 4	exlimih 1524	. 2 |- ( E. y y = x -> x = x )
6	1, 5	ax-mp 7	1 |- x = x

Syntax hints:   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1378  ax-ie2 1423  ax-8 1435  ax-17 1459  ax-i9 1463

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfequid  1630  stdpc6  1631  equcomi  1632  equveli  1682  sbid  1697  ax16i  1779  exists1  2037  vjust  2602  vex  2604  reu6  2781  nfccdeq  2813  sbc8g  2822  dfnul3  3254  rab0  3273  int0  3650  ruv  4293  relop  4504  f1eqcocnv  5451  mpt2xopoveq  5878