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  2655  vjust  3451  dfv2  3453  reu6  3699  sbc8g  3763  dfnul2  4301  ab0orv  4348  dfid3  5538  isso2i  5585  relop  5816  iotanul  6491  f1eqcocnv  7278  poxp2  8124  mpoxopoveq  8200  frecseq123  8263  ttrclselem2  9685  dfac2b  10090  konigthlem  10527  hash2prde  14441  hashge2el2difr  14452  pospo  18310  mamulid  22334  mdetdiagid  22493  alexsubALTlem3  23942  trust  24123  isppw2  27031  xmstrkgc  28819  avril1  30398  sa-abvi  32378  wlimeq12  35802  bj-ssbid2  36645  bj-ssbid1  36647  mptsnunlem  37321  ax12eq  38929  elnev  44420  ipo0  44431  ifr0  44432  tratrb  44519  tratrbVD  44843  unirnmapsn  45201  hspmbl  46620  et-equeucl  46863  resipos  48953