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

Theorem equid 2082
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, 5-Feb-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)
Assertion
Ref Expression
equid 𝑥 = 𝑥

Proof of Theorem equid
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ax7v1 2080 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 52 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 2044 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1996 1 𝑥 = 𝑥
Colors of variables: wff setvar class
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078
This theorem depends on definitions:  df-bi 197  df-ex 1842
This theorem is referenced by:  nfequid  2083  equcomiv  2084  equcomi  2087  stdpc6  2098  ax6dgen  2142  ax13dgen1  2151  ax13dgen3  2153  sbid  2249  exists1  2687  vjust  3329  vex  3331  reu6  3524  nfccdeq  3562  sbc8g  3572  dfnul3  4049  rab0OLD  4087  int0OLD  4631  dfid3  5163  isso2i  5207  relop  5416  iotanul  6015  f1eqcocnv  6707  fsplit  7438  mpt2xopoveq  7502  ruv  8660  dfac2b  9114  dfac2OLD  9116  konigthlem  9553  hash2prde  13415  hashge2el2difr  13426  pospo  17145  mamulid  20420  mdetdiagid  20579  alexsubALTlem3  22025  trust  22205  isppw2  25011  xmstrkgc  25936  avril1  27601  foo3  29582  domep  31974  wlimeq12  32041  frecseq123  32054  bj-ssbid2  32922  bj-ssbid1  32924  bj-vjust  33063  mptsnunlem  33467  ax12eq  34699  elnev  39110  ipo0  39124  ifr0  39125  tratrb  39217  tratrbVD  39565  unirnmapsn  39874  hspmbl  41318
  Copyright terms: Public domain W3C validator