Theorem equid 1689

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

Syntax hints:   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfequid  1690  stdpc6  1691  equcomi  1692  equveli  1747  sbid  1762  ax16i  1846  exists1  2110  vjust  2727  vex  2729  reu6  2915  nfccdeq  2949  sbc8g  2958  dfnul3  3412  rab0  3437  int0  3838  ruv  4527  dcextest  4558  relop  4754  f1eqcocnv  5759  mpoxopoveq  6208  snexxph  6915