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

Theorem equid 1646
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
Dummy variable  y is distinct from all other variables.

Proof of Theorem equid
StepHypRef Expression
1 ax9v 1638 . . 3  |-  -.  A. y  -.  y  =  x
2 ax-8 1645 . . . . . 6  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 45 . . . . 5  |-  ( y  =  x  ->  x  =  x )
43con3i 129 . . . 4  |-  ( -.  x  =  x  ->  -.  y  =  x
)
54alimi 1547 . . 3  |-  ( A. y  -.  x  =  x  ->  A. y  -.  y  =  x )
61, 5mto 169 . 2  |-  -.  A. y  -.  x  =  x
7 ax-17 1604 . 2  |-  ( -.  x  =  x  ->  A. y  -.  x  =  x )
86, 7mt3 173 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 5   A.wal 1528
This theorem is referenced by:  equcomi  1647  stdpc6  1651  19.2  1672  ax9dgen  1691  ax12dgen1  1700  ax12dgen3  1702  sbid  1865  equveli  1931  ax11eq  2134  exists1  2234  vjust  2791  nfccdeq  2991  sbc8g  3000  rab0  3477  dfid3  4310  reusv5OLD  4544  reusv7OLD  4546  relop  4834  fv2  5482  fsplit  6185  ruv  7310  konigthlem  8186  alexsubALTlem3  17738  isppw2  20348  avril1  20829  mathbox  23015  foo3  23016  domep  23551  dffix2  23854  elfuns  23862  vecval3b  24852  mamulid  26858  elnev  27038  ipo0  27052  ifr0  27053  a12lem1  28398
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645
  Copyright terms: Public domain W3C validator