Theorem equid 2032

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 2030	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1989	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1951	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  nfequid  2033  equcomiv  2034  equcomi  2037  stdpc6  2048  equsb1v  2139  ax6dgen  2162  ax13dgen1  2171  ax13dgen3  2173  sbid  2290  exists1  2687  vjust  3455  dfv2  3457  reu6  3689  sbc8g  3752  dfnul2  4288  dfid3  5545  isso2i  5592  relop  5822  iotanul  6501  f1eqcocnv  7285  poxp2  8123  mpoxopoveq  8199  frecseq123  8263  ttrclselem2  9681  dfac2b  10087  konigthlem  10526  hash2prde  14483  hashge2el2difr  14494  pospo  18375  mamulid  22498  mdetdiagid  22657  alexsubALTlem3  24106  trust  24286  isppw2  27176  xmstrkgc  29083  avril1  30662  sa-abvi  32643  wlimeq12  36164  bj-dfnul2  37010  bj-ssbid2  37131  bj-ssbid1  37133  mptsnunlem  37829  ax12eq  39562  elnev  45010  ipo0  45021  ifr0  45022  tratrb  45109  tratrbVD  45433  unirnmapsn  45787  hspmbl  47200  et-equeucl  47443  nprmmul3  48132  resipos  49593