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  18280  mamulid  22304  mdetdiagid  22463  alexsubALTlem3  23912  trust  24093  isppw2  27001  xmstrkgc  28789  avril1  30365  sa-abvi  32345  wlimeq12  35780  bj-ssbid2  36623  bj-ssbid1  36625  mptsnunlem  37299  ax12eq  38907  elnev  44400  ipo0  44411  ifr0  44412  tratrb  44499  tratrbVD  44823  unirnmapsn  45181  hspmbl  46600  et-equeucl  46843  resipos  48936