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

Theorem equid 1925
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 1923 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 49 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1876 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1845 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 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  nfequid  1926  equcomiv  1927  equcomi  1930  stdpc6  1943  ax6dgen  1991  ax13dgen1  2000  ax13dgen3  2002  sbid  2099  exists1  2548  vjust  3173  vex  3175  reu6  3361  nfccdeq  3399  sbc8g  3409  dfnul3  3876  rab0OLD  3909  int0OLD  4420  dfid3  4944  isso2i  4981  relop  5182  f1eqcocnv  6434  fsplit  7146  mpt2xopoveq  7209  ruv  8367  dfac2  8813  konigthlem  9246  hash2prde  13061  hashge2el2difr  13068  pospo  16742  mamulid  20008  mdetdiagid  20167  alexsubALTlem3  21605  trust  21785  isppw2  24558  xmstrkgc  25484  nbgranself  25729  usgrasscusgra  25777  rusgrasn  26238  avril1  26477  foo3  28492  domep  30748  wlimeq12  30815  bj-ssbid2  31640  bj-ssbid1  31642  bj-vjust  31780  mptsnunlem  32157  ax12eq  33040  elnev  37457  ipo0  37470  ifr0  37471  tratrb  37563  tratrbVD  37915  unirnmapsn  38197  hspmbl  39316
  Copyright terms: Public domain W3C validator