Theorem equid 2016

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, 22-Aug-2020.)

Assertion

Ref	Expression
equid	⊢ 𝑥 = 𝑥

Proof of Theorem equid

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax7v1 2014	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1974	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1935	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  nfequid  2017  equcomiv  2018  equcomi  2021  stdpc6  2032  equsb1v  2104  ax6dgen  2125  ax13dgen1  2134  ax13dgen3  2136  sbid  2248  exists1  2657  vjust  3476  dfv2  3478  vexOLD  3480  reu6  3723  sbc8g  3786  dfnul2  4326  dfnul2OLD  4328  dfnul3OLD  4329  dfnul4OLD  4330  ab0orv  4379  dfid3  5578  isso2i  5624  relop  5851  iotanul  6522  f1eqcocnv  7299  f1eqcocnvOLD  7300  poxp2  8129  mpoxopoveq  8204  frecseq123  8267  ttrclselem2  9721  dfac2b  10125  konigthlem  10563  hash2prde  14431  hashge2el2difr  14442  pospo  18298  mamulid  21943  mdetdiagid  22102  alexsubALTlem3  23553  trust  23734  isppw2  26619  xmstrkgc  28143  avril1  29716  sa-abvi  31696  wlimeq12  34791  bj-ssbid2  35539  bj-ssbid1  35541  mptsnunlem  36219  ax12eq  37811  elnev  43197  ipo0  43208  ifr0  43209  tratrb  43297  tratrbVD  43622  unirnmapsn  43913  hspmbl  45345  et-equeucl  45588