Theorem equid 2012

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  nfequid  2013  equcomiv  2014  equcomi  2017  stdpc6  2028  equsb1v  2106  ax6dgen  2129  ax13dgen1  2138  ax13dgen3  2140  sbid  2256  exists1  2654  vjust  3445  dfv2  3447  reu6  3694  sbc8g  3758  dfnul2  4295  ab0orv  4342  dfid3  5529  isso2i  5576  relop  5804  iotanul  6477  f1eqcocnv  7258  poxp2  8099  mpoxopoveq  8175  frecseq123  8238  ttrclselem2  9655  dfac2b  10060  konigthlem  10497  hash2prde  14411  hashge2el2difr  14422  pospo  18284  mamulid  22361  mdetdiagid  22520  alexsubALTlem3  23969  trust  24150  isppw2  27058  xmstrkgc  28866  avril1  30442  sa-abvi  32422  wlimeq12  35800  bj-ssbid2  36643  bj-ssbid1  36645  mptsnunlem  37319  ax12eq  38927  elnev  44420  ipo0  44431  ifr0  44432  tratrb  44519  tratrbVD  44843  unirnmapsn  45201  hspmbl  46620  et-equeucl  46863  resipos  48956