Theorem equid 1630

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

Syntax hints:   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfequid  1631  stdpc6  1632  equcomi  1633  equveli  1684  sbid  1699  ax16i  1781  exists1  2039  vjust  2611  vex  2613  reu6  2791  nfccdeq  2823  sbc8g  2832  dfnul3  3271  rab0  3290  int0  3671  ruv  4322  relop  4535  f1eqcocnv  5483  mpt2xopoveq  5910