Theorem equid 2045

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nfequid  2046  equcomiv  2047  equcomi  2050  stdpc6  2061  equsb1v  2143  ax6dgen  2166  ax13dgen1  2175  ax13dgen3  2177  sbid  2293  exists1  2690  vjust  3458  dfv2  3460  reu6  3691  sbc8g  3754  dfnul2  4289  dfid3  5561  isso2i  5608  relop  5838  iotanul  6520  f1eqcocnv  7308  poxp2  8145  mpoxopoveq  8221  frecseq123  8285  ttrclselem2  9702  dfac2b  10130  konigthlem  10568  hash2prde  14525  hashge2el2difr  14536  pospo  18421  mamulid  22648  mdetdiagid  22807  alexsubALTlem3  24257  trust  24437  isppw2  27330  xmstrkgc  29290  avril1  30885  sa-abvi  32866  wlimeq12  36346  bj-dfnul2  37220  bj-ssbid2  37341  bj-ssbid1  37343  mptsnunlem  38041  ax12eq  39773  elnev  45205  ipo0  45216  ifr0  45217  tratrb  45303  tratrbVD  45627  unirnmapsn  45988  hspmbl  47401  et-equeucl  47644  nprmmul3  48336  resipos  49810