Theorem equid 2044

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  nfequid  2045  equcomiv  2046  equcomi  2049  stdpc6  2060  equsb1v  2141  ax6dgen  2164  ax13dgen1  2173  ax13dgen3  2175  sbid  2290  exists1  2685  vjust  3451  dfv2  3453  reu6  3683  sbc8g  3746  dfnul2  4280  dfid3  5549  isso2i  5596  relop  5829  iotanul  6522  f1eqcocnv  7313  poxp2  8166  mpoxopoveq  8243  frecseq123  8307  ttrclselem2  9734  dfac2b  10216  konigthlem  10660  hash2prde  14622  hashge2el2difr  14633  pospo  18526  mamulid  22765  mdetdiagid  22924  alexsubALTlem3  24377  trust  24557  isppw2  27451  xmstrkgc  29472  avril1  31073  sa-abvi  33096  reu6f  35759  wlimeq12  36677  bj-dfnul2  37536  bj-ssbid2  37657  bj-ssbid1  37659  mptsnunlem  38370  ax12eq  40107  elnev  45529  ipo0  45540  ifr0  45541  tratrb  45627  tratrbVD  45951  unirnmapsn  46335  hspmbl  47747  et-equeucl  47990  nprmmul3  48719  resipos  50197