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

Theorem equid 2097
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 2095 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 52 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 2059 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 2011 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 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  nfequid  2098  equcomiv  2099  equcomi  2102  stdpc6  2113  ax6dgen  2160  ax13dgen1  2169  ax13dgen3  2171  sbid  2270  exists1  2710  vjust  3352  vex  3354  reu6  3547  nfccdeq  3585  sbc8g  3595  dfnul3  4066  dfid3  5159  isso2i  5203  relop  5410  iotanul  6008  f1eqcocnv  6701  fsplit  7436  mpt2xopoveq  7500  ruv  8666  dfac2b  9156  dfac2OLD  9158  konigthlem  9595  hash2prde  13453  hashge2el2difr  13464  pospo  17180  mamulid  20463  mdetdiagid  20623  alexsubALTlem3  22072  trust  22252  isppw2  25061  xmstrkgc  25986  avril1  27660  foo3  29641  domep  32033  wlimeq12  32100  frecseq123  32113  bj-ssbid2  32981  bj-ssbid1  32983  bj-vjust  33121  mptsnunlem  33521  ax12eq  34748  elnev  39165  ipo0  39178  ifr0  39179  tratrb  39271  tratrbVD  39619  unirnmapsn  39923  hspmbl  41360
  Copyright terms: Public domain W3C validator