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

Theorem equid 2012
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, 22-Aug-2020.)
Assertion
Ref Expression
equid 𝑥 = 𝑥

Proof of Theorem equid
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ax7v1 2010 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 52 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1965 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1925 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 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008
This theorem depends on definitions:  df-bi 209  df-ex 1774
This theorem is referenced by:  nfequid  2013  equcomiv  2014  equcomi  2017  stdpc6  2028  equsb1v  2105  ax6dgen  2125  ax13dgen1  2134  ax13dgen3  2136  sbid  2249  exists1  2742  vjust  3494  vex  3496  vexOLD  3497  reu6  3715  sbc8g  3778  dfnul2  4291  dfnul3  4293  dfid3  5455  isso2i  5501  relop  5714  domepOLD  5787  iotanul  6326  f1eqcocnv  7049  fsplitOLD  7805  mpoxopoveq  7877  ruv  9058  dfac2b  9548  konigthlem  9982  hash2prde  13820  hashge2el2difr  13831  pospo  17575  mamulid  21042  mdetdiagid  21201  alexsubALTlem3  22649  trust  22830  isppw2  25684  xmstrkgc  26664  avril1  28234  sa-abvi  30212  wlimeq12  33094  frecseq123  33107  bj-ssbid2  33983  bj-ssbid1  33985  mptsnunlem  34606  ax12eq  36064  elnev  40755  ipo0  40766  ifr0  40767  tratrb  40855  tratrbVD  41180  unirnmapsn  41461  hspmbl  42896
  Copyright terms: Public domain W3C validator