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  2291  exists1  2686  vjust  3452  dfv2  3454  reu6  3684  sbc8g  3747  dfnul2  4282  dfid3  5549  isso2i  5596  relop  5828  iotanul  6517  f1eqcocnv  7307  poxp2  8153  mpoxopoveq  8229  frecseq123  8293  ttrclselem2  9720  dfac2b  10202  konigthlem  10646  hash2prde  14608  hashge2el2difr  14619  pospo  18510  mamulid  22749  mdetdiagid  22908  alexsubALTlem3  24361  trust  24541  isppw2  27435  xmstrkgc  29456  avril1  31057  sa-abvi  33038  wlimeq12  36561  bj-dfnul2  37420  bj-ssbid2  37541  bj-ssbid1  37543  mptsnunlem  38241  ax12eq  39978  elnev  45406  ipo0  45417  ifr0  45418  tratrb  45504  tratrbVD  45828  unirnmapsn  46196  hspmbl  47608  et-equeucl  47851  nprmmul3  48580  resipos  50052