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  2262  exists1  2661  vjust  3441  dfv2  3443  reu6  3684  sbc8g  3748  dfnul2  4288  dfid3  5522  isso2i  5569  relop  5799  iotanul  6472  f1eqcocnv  7247  poxp2  8085  mpoxopoveq  8161  frecseq123  8224  ttrclselem2  9635  dfac2b  10041  konigthlem  10479  hash2prde  14393  hashge2el2difr  14404  pospo  18266  mamulid  22385  mdetdiagid  22544  alexsubALTlem3  23993  trust  24173  isppw2  27081  xmstrkgc  28958  avril1  30538  sa-abvi  32518  wlimeq12  36011  bj-ssbid2  36863  bj-ssbid1  36865  mptsnunlem  37543  ax12eq  39201  elnev  44678  ipo0  44689  ifr0  44690  tratrb  44777  tratrbVD  45101  unirnmapsn  45458  hspmbl  46873  et-equeucl  47116  resipos  49220