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  2142  ax6dgen  2165  ax13dgen1  2174  ax13dgen3  2176  sbid  2290  exists1  2685  vjust  3451  dfv2  3453  reu6  3684  sbc8g  3747  dfnul2  4282  dfid3  5553  isso2i  5600  relop  5830  iotanul  6513  f1eqcocnv  7302  poxp2  8141  mpoxopoveq  8217  frecseq123  8281  ttrclselem2  9705  dfac2b  10133  konigthlem  10577  hash2prde  14535  hashge2el2difr  14546  pospo  18431  mamulid  22663  mdetdiagid  22822  alexsubALTlem3  24275  trust  24455  isppw2  27351  xmstrkgc  29342  avril1  30943  sa-abvi  32924  wlimeq12  36396  bj-dfnul2  37271  bj-ssbid2  37392  bj-ssbid1  37394  mptsnunlem  38092  ax12eq  39814  elnev  45261  ipo0  45272  ifr0  45273  tratrb  45359  tratrbVD  45683  unirnmapsn  46044  hspmbl  47457  et-equeucl  47700  nprmmul3  48429  resipos  49901