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  3191  vex  3193  reu6  3382  nfccdeq  3420  sbc8g  3430  dfnul3  3900  rab0OLD  3936  int0OLD  4463  dfid3  5000  isso2i  5037  relop  5242  iotanul  5835  f1eqcocnv  6521  fsplit  7242  mpt2xopoveq  7305  ruv  8467  dfac2  8913  konigthlem  9350  hash2prde  13206  hashge2el2difr  13217  pospo  16913  mamulid  20187  mdetdiagid  20346  alexsubALTlem3  21793  trust  21973  isppw2  24775  xmstrkgc  25700  avril1  27207  foo3  29190  domep  31452  wlimeq12  31519  bj-ssbid2  32340  bj-ssbid1  32342  bj-vjust  32482  mptsnunlem  32856  ax12eq  33745  elnev  38160  ipo0  38174  ifr0  38175  tratrb  38267  tratrbVD  38619  unirnmapsn  38915  hspmbl  40180
  Copyright terms: Public domain W3C validator