Theorem equid 2016

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  nfequid  2017  equcomiv  2018  equcomi  2021  stdpc6  2032  equsb1v  2105  ax6dgen  2126  ax13dgen1  2135  ax13dgen3  2137  sbid  2251  exists1  2662  vjust  3423  dfv2  3425  vexOLD  3427  reu6  3656  sbc8g  3719  dfnul2  4256  dfnul2OLD  4258  dfnul3OLD  4259  dfnul4OLD  4260  ab0orv  4309  dfid3  5483  isso2i  5529  relop  5748  domepOLD  5822  iotanul  6396  f1eqcocnv  7153  f1eqcocnvOLD  7154  fsplitOLD  7929  mpoxopoveq  8006  frecseq123  8069  dfac2b  9817  konigthlem  10255  hash2prde  14112  hashge2el2difr  14123  pospo  17978  mamulid  21498  mdetdiagid  21657  alexsubALTlem3  23108  trust  23289  isppw2  26169  xmstrkgc  27156  avril1  28728  sa-abvi  30706  ttrclselem2  33712  poxp2  33717  wlimeq12  33740  bj-ssbid2  34770  bj-ssbid1  34772  mptsnunlem  35436  ax12eq  36882  elnev  41945  ipo0  41956  ifr0  41957  tratrb  42045  tratrbVD  42370  unirnmapsn  42643  hspmbl  44057