Theorem equid 2013

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  nfequid  2014  equcomiv  2015  equcomi  2018  stdpc6  2029  equsb1v  2110  ax6dgen  2133  ax13dgen1  2142  ax13dgen3  2144  sbid  2260  exists1  2659  vjust  3439  dfv2  3441  reu6  3682  sbc8g  3746  dfnul2  4286  dfid3  5520  isso2i  5567  relop  5797  iotanul  6470  f1eqcocnv  7245  poxp2  8083  mpoxopoveq  8159  frecseq123  8222  ttrclselem2  9633  dfac2b  10039  konigthlem  10477  hash2prde  14391  hashge2el2difr  14402  pospo  18264  mamulid  22383  mdetdiagid  22542  alexsubALTlem3  23991  trust  24171  isppw2  27079  xmstrkgc  28907  avril1  30487  sa-abvi  32467  wlimeq12  35960  bj-ssbid2  36806  bj-ssbid1  36808  mptsnunlem  37482  ax12eq  39140  elnev  44620  ipo0  44631  ifr0  44632  tratrb  44719  tratrbVD  45043  unirnmapsn  45400  hspmbl  46815  et-equeucl  47058  resipos  49162