Theorem equid 2042

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 2040	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 53	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1999	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1961	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

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

This theorem is referenced by:  nfequid  2043  equcomiv  2044  equcomi  2047  stdpc6  2058  equsb1v  2140  ax6dgen  2163  ax13dgen1  2172  ax13dgen3  2174  sbid  2291  exists1  2688  vjust  3456  dfv2  3458  reu6  3689  sbc8g  3752  dfnul2  4289  dfid3  5559  isso2i  5606  relop  5836  iotanul  6516  f1eqcocnv  7299  poxp2  8135  mpoxopoveq  8211  frecseq123  8275  ttrclselem2  9691  dfac2b  10110  konigthlem  10548  hash2prde  14503  hashge2el2difr  14514  pospo  18394  mamulid  22598  mdetdiagid  22757  alexsubALTlem3  24206  trust  24386  isppw2  27279  xmstrkgc  29235  avril1  30814  sa-abvi  32795  wlimeq12  36309  bj-dfnul2  37163  bj-ssbid2  37284  bj-ssbid1  37286  mptsnunlem  37984  ax12eq  39715  elnev  45147  ipo0  45158  ifr0  45159  tratrb  45245  tratrbVD  45569  unirnmapsn  45930  hspmbl  47343  et-equeucl  47586  nprmmul3  48278  resipos  49753