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

Theorem equid 1644
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 1636 . . 3  |-  -.  A. y  -.  y  =  x
2 ax-8 1643 . . . . . 6  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 43 . . . . 5  |-  ( y  =  x  ->  x  =  x )
43con3i 127 . . . 4  |-  ( -.  x  =  x  ->  -.  y  =  x
)
54alimi 1546 . . 3  |-  ( A. y  -.  x  =  x  ->  A. y  -.  y  =  x )
61, 5mto 167 . 2  |-  -.  A. y  -.  x  =  x
7 ax-17 1603 . 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 1527
This theorem is referenced by:  nfequid  1645  equcomi  1646  stdpc6  1650  19.2  1671  ax9dgen  1690  ax12dgen1  1699  ax12dgen3  1701  sbid  1863  equveli  1928  ax11eq  2132  exists1  2232  vjust  2789  nfccdeq  2989  sbc8g  2998  rab0  3475  dfid3  4310  reusv5OLD  4544  reusv7OLD  4546  relop  4834  fsplit  6223  ruv  7314  konigthlem  8190  alexsubALTlem3  17743  isppw2  20353  avril1  20836  mathbox  23022  foo3  23023  iuninc  23158  measiuns  23544  domep  24149  dffix2  24445  vecval3b  25452  mamulid  27458  elnev  27638  ipo0  27652  ifr0  27653  mpt2xopoveq  28085  nbgranself  28149  tratrb  28299  tratrbVD  28637  a12lem1  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
  Copyright terms: Public domain W3C validator