NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  equid GIF version

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.
StepHypRef Expression
1 a9ev 1656 . 2 y y = x
2 ax-8 1675 . . . 4 (y = x → (y = xx = x))
32pm2.43i 43 . . 3 (y = xx = x)
43eximi 1576 . 2 (y y = xy x = x)
5 ax17e 1618 . 2 (y x = xx = x)
61, 4, 5mp2b 9 1 x = x
Colors of variables: wff setvar class
Syntax hints:  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  2860  sbc8g  3053  rab0  3571  dfid3  4768  fvi  5442  2ndfo  5506
  Copyright terms: Public domain W3C validator