Theorem equid 1676

Description: Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 9-Dec-2017.)

Assertion

Ref	Expression
equid	|- x = x

Proof of Theorem equid

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		a9ev 1656	. 2 |- E.y y = x
2		ax-8 1675	. . . 4 |- (y = x -> (y = x -> x = x))
3	2	pm2.43i 43	. . 3 |- (y = x -> x = x)
4	3	eximi 1576	. 2 |- (E.y y = x -> E.y x = x)
5		ax17e 1618	. 2 |- (E.y x = x -> x = x)
6	1, 4, 5	mp2b 9	1 |- x = x

Syntax hints:  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  nfequid  1678  equcomi  1679  stdpc6  1687  19.2OLD  1700  ax9dgen  1716  ax12dgen1  1725  ax12dgen3  1727  sbid  1922  equveli  1988  ax11eq  2193  exists1  2293  vjust  2861  sbc8g  3054  rab0  3572  dfid3  4769  fvi  5443  2ndfo  5507