Theorem equid 2014

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  nfequid  2015  equcomiv  2016  equcomi  2019  stdpc6  2030  equsb1v  2111  ax6dgen  2134  ax13dgen1  2143  ax13dgen3  2145  sbid  2263  exists1  2662  vjust  3443  dfv2  3445  reu6  3686  sbc8g  3750  dfnul2  4290  dfid3  5530  isso2i  5577  relop  5807  iotanul  6480  f1eqcocnv  7257  poxp2  8095  mpoxopoveq  8171  frecseq123  8234  ttrclselem2  9647  dfac2b  10053  konigthlem  10491  hash2prde  14405  hashge2el2difr  14416  pospo  18278  mamulid  22397  mdetdiagid  22556  alexsubALTlem3  24005  trust  24185  isppw2  27093  xmstrkgc  28970  avril1  30550  sa-abvi  32531  wlimeq12  36033  bj-dfnul2  36795  bj-ssbid2  36907  bj-ssbid1  36909  mptsnunlem  37593  ax12eq  39317  elnev  44793  ipo0  44804  ifr0  44805  tratrb  44892  tratrbVD  45216  unirnmapsn  45572  hspmbl  46987  et-equeucl  47230  resipos  49334