Theorem equid 2013

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  nfequid  2014  equcomiv  2015  equcomi  2018  stdpc6  2029  equsb1v  2108  ax6dgen  2131  ax13dgen1  2140  ax13dgen3  2142  sbid  2258  exists1  2656  vjust  3437  dfv2  3439  reu6  3680  sbc8g  3744  dfnul2  4283  dfid3  5512  isso2i  5559  relop  5789  iotanul  6461  f1eqcocnv  7235  poxp2  8073  mpoxopoveq  8149  frecseq123  8212  ttrclselem2  9616  dfac2b  10022  konigthlem  10459  hash2prde  14377  hashge2el2difr  14388  pospo  18249  mamulid  22356  mdetdiagid  22515  alexsubALTlem3  23964  trust  24144  isppw2  27052  xmstrkgc  28864  avril1  30443  sa-abvi  32423  wlimeq12  35861  bj-ssbid2  36704  bj-ssbid1  36706  mptsnunlem  37380  ax12eq  38988  elnev  44478  ipo0  44489  ifr0  44490  tratrb  44577  tratrbVD  44901  unirnmapsn  45259  hspmbl  46675  et-equeucl  46918  resipos  49014