Theorem equid 1939

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  nfequid  1940  equcomiv  1941  equcomi  1944  stdpc6  1957  ax6dgen  2005  ax13dgen1  2014  ax13dgen3  2016  sbid  2114  exists1  2561  vjust  3201  vex  3203  reu6  3395  nfccdeq  3433  sbc8g  3443  dfnul3  3918  rab0OLD  3956  int0OLD  4491  dfid3  5025  isso2i  5067  relop  5272  iotanul  5866  f1eqcocnv  6556  fsplit  7282  mpt2xopoveq  7345  ruv  8507  dfac2  8953  konigthlem  9390  hash2prde  13252  hashge2el2difr  13263  pospo  16973  mamulid  20247  mdetdiagid  20406  alexsubALTlem3  21853  trust  22033  isppw2  24841  xmstrkgc  25766  avril1  27319  foo3  29302  domep  31698  wlimeq12  31765  bj-ssbid2  32645  bj-ssbid1  32647  bj-vjust  32786  mptsnunlem  33185  ax12eq  34226  elnev  38639  ipo0  38653  ifr0  38654  tratrb  38746  tratrbVD  39097  unirnmapsn  39406  hspmbl  40843