Theorem equid 2039

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

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

This theorem is referenced by:  nfequid  2040  equcomiv  2041  equcomi  2044  stdpc6  2055  equsb1v  2146  ax6dgen  2169  ax13dgen1  2178  ax13dgen3  2180  sbid  2297  exists1  2694  vjust  3464  dfv2  3466  reu6  3698  sbc8g  3761  dfnul2  4297  dfid3  5560  isso2i  5607  relop  5837  iotanul  6517  f1eqcocnv  7300  poxp2  8138  mpoxopoveq  8214  frecseq123  8278  ttrclselem2  9694  dfac2b  10113  konigthlem  10552  hash2prde  14506  hashge2el2difr  14517  pospo  18398  mamulid  22566  mdetdiagid  22725  alexsubALTlem3  24174  trust  24354  isppw2  27244  xmstrkgc  29175  avril1  30754  sa-abvi  32735  wlimeq12  36207  bj-dfnul2  37051  bj-ssbid2  37172  bj-ssbid1  37174  mptsnunlem  37871  ax12eq  39604  elnev  45038  ipo0  45049  ifr0  45050  tratrb  45136  tratrbVD  45460  unirnmapsn  45821  hspmbl  47234  et-equeucl  47477  nprmmul3  48166  resipos  49637