MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equid Unicode version

Theorem equid 1662
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.)
Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ax9v 1645 . . 3  |-  -.  A. y  -.  y  =  x
2 ax-8 1661 . . . . . 6  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 43 . . . . 5  |-  ( y  =  x  ->  x  =  x )
43con3i 127 . . . 4  |-  ( -.  x  =  x  ->  -.  y  =  x
)
54alimi 1549 . . 3  |-  ( A. y  -.  x  =  x  ->  A. y  -.  y  =  x )
61, 5mto 167 . 2  |-  -.  A. y  -.  x  =  x
7 ax-17 1606 . 2  |-  ( -.  x  =  x  ->  A. y  -.  x  =  x )
86, 7mt3 171 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1530
This theorem is referenced by:  nfequid  1663  equcomi  1664  stdpc6  1670  19.2OLD  1686  ax9dgen  1702  ax12dgen1  1711  ax12dgen3  1713  sbid  1875  equveli  1941  ax11eq  2145  exists1  2245  vjust  2802  nfccdeq  3002  sbc8g  3011  rab0  3488  dfid3  4326  reusv5OLD  4560  reusv7OLD  4562  relop  4850  fsplit  6239  ruv  7330  konigthlem  8206  alexsubALTlem3  17759  isppw2  20369  avril1  20852  mathbox  23038  foo3  23039  iuninc  23174  measiuns  23559  domep  24220  dffix2  24516  vecval3b  25555  mamulid  27561  elnev  27741  ipo0  27755  ifr0  27756  mpt2xopoveq  28201  nbgranself  28283  tratrb  28598  tratrbVD  28953  equveliNEW7  29503  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661
  Copyright terms: Public domain W3C validator