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

Theorem equid 1645
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 1637 . . 3  |-  -.  A. y  -.  y  =  x
2 ax-8 1644 . . . . . 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  1646  equcomi  1647  stdpc6  1651  19.2  1672  ax9dgen  1691  ax12dgen1  1700  ax12dgen3  1702  sbid  1865  equveli  1931  ax11eq  2133  exists1  2233  vjust  2790  nfccdeq  2990  sbc8g  2999  rab0  3476  dfid3  4309  reusv5OLD  4543  reusv7OLD  4545  relop  4833  fv2  5482  fsplit  6185  ruv  7310  konigthlem  8186  alexsubALTlem3  17739  isppw2  20349  avril1  20830  mathbox  23018  foo3  23019  domep  23553  dffix2  23856  elfuns  23864  vecval3b  24863  mamulid  26869  elnev  27049  ipo0  27063  ifr0  27064  tratrb  27582  tratrbVD  27917  a12lem1  28409
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 1636  ax-8 1644
  Copyright terms: Public domain W3C validator