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

Theorem equid 1936
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 1934 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 52 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1887 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1856 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 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  nfequid  1937  equcomiv  1938  equcomi  1941  stdpc6  1954  ax6dgen  2002  ax13dgen1  2011  ax13dgen3  2013  sbid  2111  exists1  2560  vjust  3187  vex  3189  reu6  3377  nfccdeq  3415  sbc8g  3425  dfnul3  3894  rab0OLD  3930  int0OLD  4456  dfid3  4990  isso2i  5027  relop  5232  iotanul  5825  f1eqcocnv  6510  fsplit  7227  mpt2xopoveq  7290  ruv  8451  dfac2  8897  konigthlem  9334  hash2prde  13190  hashge2el2difr  13201  pospo  16894  mamulid  20166  mdetdiagid  20325  alexsubALTlem3  21763  trust  21943  isppw2  24741  xmstrkgc  25666  avril1  27173  foo3  29148  domep  31396  wlimeq12  31463  bj-ssbid2  32284  bj-ssbid1  32286  bj-vjust  32426  mptsnunlem  32814  ax12eq  33703  elnev  38118  ipo0  38132  ifr0  38133  tratrb  38225  tratrbVD  38577  unirnmapsn  38877  hspmbl  40147
  Copyright terms: Public domain W3C validator