Theorem equid 2020

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016

This theorem depends on definitions:  df-bi 210  df-ex 1783

This theorem is referenced by:  nfequid  2021  equcomiv  2022  equcomi  2025  stdpc6  2036  equsb1v  2110  ax6dgen  2130  ax13dgen1  2139  ax13dgen3  2141  sbid  2255  exists1  2683  vjust  3411  dfv2  3413  vexOLD  3415  reu6  3641  sbc8g  3705  dfnul2  4228  dfnul3  4229  dfnul4  4230  ab0orv  4276  dfid3  5433  isso2i  5478  relop  5691  domepOLD  5766  iotanul  6314  f1eqcocnv  7050  f1eqcocnvOLD  7051  fsplitOLD  7819  mpoxopoveq  7896  dfac2b  9591  konigthlem  10029  hash2prde  13881  hashge2el2difr  13892  pospo  17650  mamulid  21142  mdetdiagid  21301  alexsubALTlem3  22750  trust  22931  isppw2  25800  xmstrkgc  26780  avril1  28348  sa-abvi  30326  poxp2  33346  wlimeq12  33368  frecseq123  33381  bj-ssbid2  34390  bj-ssbid1  34392  mptsnunlem  35036  ax12eq  36518  elnev  41516  ipo0  41527  ifr0  41528  tratrb  41616  tratrbVD  41941  unirnmapsn  42214  hspmbl  43635