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  3720  sbc8g  3783  dfnul2  4323  dfnul2OLD  4325  dfnul3OLD  4326  dfnul4OLD  4327  ab0orv  4376  dfid3  5573  isso2i  5619  relop  5845  iotanul  6513  f1eqcocnv  7286  f1eqcocnvOLD  7287  poxp2  8116  mpoxopoveq  8191  frecseq123  8254  ttrclselem2  9708  dfac2b  10112  konigthlem  10550  hash2prde  14418  hashge2el2difr  14429  pospo  18285  mamulid  21912  mdetdiagid  22071  alexsubALTlem3  23522  trust  23703  isppw2  26586  xmstrkgc  28110  avril1  29683  sa-abvi  31661  wlimeq12  34722  bj-ssbid2  35444  bj-ssbid1  35446  mptsnunlem  36124  ax12eq  37717  elnev  43068  ipo0  43079  ifr0  43080  tratrb  43168  tratrbVD  43493  unirnmapsn  43784  hspmbl  45218  et-equeucl  45461