Theorem equid 2010

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 2008	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1968	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1930	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  nfequid  2011  equcomiv  2012  equcomi  2015  stdpc6  2026  equsb1v  2104  ax6dgen  2127  ax13dgen1  2136  ax13dgen3  2138  sbid  2254  exists1  2659  vjust  3458  dfv2  3460  reu6  3707  sbc8g  3771  dfnul2  4309  ab0orv  4356  dfid3  5549  isso2i  5596  relop  5828  iotanul  6506  f1eqcocnv  7290  poxp2  8137  mpoxopoveq  8213  frecseq123  8276  ttrclselem2  9733  dfac2b  10138  konigthlem  10575  hash2prde  14478  hashge2el2difr  14489  pospo  18342  mamulid  22366  mdetdiagid  22525  alexsubALTlem3  23974  trust  24155  isppw2  27063  xmstrkgc  28799  avril1  30378  sa-abvi  32358  wlimeq12  35766  bj-ssbid2  36609  bj-ssbid1  36611  mptsnunlem  37285  ax12eq  38888  elnev  44395  ipo0  44406  ifr0  44407  tratrb  44494  tratrbVD  44819  unirnmapsn  45172  hspmbl  46594  et-equeucl  46837  resipos  48843