Theorem equid 2011

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  nfequid  2012  equcomiv  2013  equcomi  2016  stdpc6  2027  equsb1v  2105  ax6dgen  2128  ax13dgen1  2137  ax13dgen3  2139  sbid  2256  exists1  2664  vjust  3489  dfv2  3491  reu6  3748  sbc8g  3812  dfnul2  4355  dfnul2OLD  4357  dfnul3OLD  4358  dfnul4OLD  4359  ab0orv  4406  dfid3  5596  isso2i  5642  relop  5870  iotanul  6546  f1eqcocnv  7332  poxp2  8178  mpoxopoveq  8254  frecseq123  8317  ttrclselem2  9789  dfac2b  10194  konigthlem  10631  hash2prde  14513  hashge2el2difr  14524  pospo  18409  mamulid  22460  mdetdiagid  22619  alexsubALTlem3  24070  trust  24251  isppw2  27168  xmstrkgc  28910  avril1  30487  sa-abvi  32467  wlimeq12  35775  bj-ssbid2  36620  bj-ssbid1  36622  mptsnunlem  37296  ax12eq  38889  elnev  44402  ipo0  44413  ifr0  44414  tratrb  44502  tratrbVD  44827  unirnmapsn  45110  hspmbl  46539  et-equeucl  46782