Theorem equid 2041

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037

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

This theorem is used by:  nfequid  2042  equcomiv  2043  equcomi  2046  stdpc6  2057  equsb1v  2139  ax6dgen  2162  ax13dgen1  2171  ax13dgen3  2173  sbid  2290  exists1  2687  vjust  3455  dfv2  3457  reu6  3688  sbc8g  3751  dfnul2  4288  dfid3  5558  isso2i  5605  relop  5835  iotanul  6516  f1eqcocnv  7299  poxp2  8137  mpoxopoveq  8213  frecseq123  8277  ttrclselem2  9693  dfac2b  10121  konigthlem  10559  hash2prde  14514  hashge2el2difr  14525  pospo  18405  mamulid  22609  mdetdiagid  22768  alexsubALTlem3  24217  trust  24397  isppw2  27290  xmstrkgc  29246  avril1  30825  sa-abvi  32806  wlimeq12  36317  bj-dfnul2  37191  bj-ssbid2  37312  bj-ssbid1  37314  mptsnunlem  38012  ax12eq  39743  elnev  45175  ipo0  45186  ifr0  45187  tratrb  45273  tratrbVD  45597  unirnmapsn  45958  hspmbl  47371  et-equeucl  47614  nprmmul3  48306  resipos  49781