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

Theorem equid 1887
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 1885 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 49 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1838 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1808 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 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883
This theorem depends on definitions:  df-bi 192  df-ex 1693
This theorem is referenced by:  nfequid  1889  equcomiv  1890  equcomi  1893  stdpc6  1906  ax6dgen  1952  ax13dgen1  1961  ax13dgen3  1963  sbid  2134  exists1  2444  vjust  3067  vex  3069  reu6  3251  nfccdeq  3289  sbc8g  3299  dfnul3  3760  rab0  3791  int0  4278  dfid3  4796  isso2i  4833  relop  5032  f1eqcocnv  6270  fsplit  6980  mpt2xopoveq  7043  ruv  8200  dfac2  8646  konigthlem  9078  hash2prde  12754  hashge2el2difr  12761  pospo  16384  mamulid  19624  mdetdiagid  19783  alexsubALTlem3  21222  trust  21402  isppw2  24203  xmstrkgc  25077  nbgranself  25323  usgrasscusgra  25372  rusgrasn  25833  avril1  26061  foo3  28259  domep  30590  wlimeq12  30653  bj-ssbid2  31440  bj-ssbid1  31442  bj-vjust  31583  mptsnunlem  31961  ax12eq  32745  elnev  37146  ipo0  37159  ifr0  37160  tratrb  37253  tratrbVD  37606  unirnmapsn  37854  hspmbl  38914
  Copyright terms: Public domain W3C validator