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

Theorem equid 1889
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 1887 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 49 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1840 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1812 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 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  nfequid  1890  equcomiv  1891  equcomi  1894  stdpc6  1907  ax6dgen  1953  ax13dgen1  1962  ax13dgen3  1964  sbid  2133  exists1  2453  vjust  3078  vex  3080  reu6  3266  nfccdeq  3304  sbc8g  3314  dfnul3  3780  rab0OLD  3813  int0OLD  4324  dfid3  4848  isso2i  4885  relop  5086  f1eqcocnv  6332  fsplit  7043  mpt2xopoveq  7106  ruv  8265  dfac2  8711  konigthlem  9144  hash2prde  12972  hashge2el2difr  12979  pospo  16686  mamulid  19967  mdetdiagid  20126  alexsubALTlem3  21564  trust  21744  isppw2  24531  xmstrkgc  25457  nbgranself  25702  usgrasscusgra  25750  rusgrasn  26211  avril1  26450  foo3  28475  domep  30785  wlimeq12  30848  bj-ssbid2  31669  bj-ssbid1  31671  bj-vjust  31816  mptsnunlem  32193  ax12eq  33119  elnev  37543  ipo0  37556  ifr0  37557  tratrb  37649  tratrbVD  38001  unirnmapsn  38285  hspmbl  39413
  Copyright terms: Public domain W3C validator