Theorem equid 1753

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

Syntax hints:   E.wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfequid  1754  stdpc6  1755  equcomi  1756  equveli  1812  sbid  1827  ax16i  1911  exists1  2183  vjust  2822  vex  2824  reu6  3015  nfccdeq  3049  sbc8g  3059  dfnul2  3523  rab0  3551  int0  3979  ruv  4692  dcextest  4723  relop  4925  f1eqcocnv  5987  mpoxopoveq  6501  snexxph  7257