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 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 2007

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

This theorem is referenced by:  nfequid  2012  equcomiv  2013  equcomi  2016  stdpc6  2027  equsb1v  2105  ax6dgen  2128  ax13dgen1  2137  ax13dgen3  2139  sbid  2255  exists1  2660  vjust  3480  dfv2  3482  reu6  3731  sbc8g  3795  dfnul2  4335  ab0orv  4382  dfid3  5579  isso2i  5627  relop  5859  iotanul  6537  f1eqcocnv  7319  poxp2  8164  mpoxopoveq  8240  frecseq123  8303  ttrclselem2  9762  dfac2b  10167  konigthlem  10604  hash2prde  14505  hashge2el2difr  14516  pospo  18386  mamulid  22437  mdetdiagid  22596  alexsubALTlem3  24047  trust  24228  isppw2  27148  xmstrkgc  28890  avril1  30472  sa-abvi  32452  wlimeq12  35798  bj-ssbid2  36641  bj-ssbid1  36643  mptsnunlem  37317  ax12eq  38920  elnev  44435  ipo0  44446  ifr0  44447  tratrb  44534  tratrbVD  44859  unirnmapsn  45192  hspmbl  46617  et-equeucl  46860