Theorem equid 2015

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 2013	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1973	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1934	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 1913  ax-6 1971  ax-7 2011

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

This theorem is referenced by:  nfequid  2016  equcomiv  2017  equcomi  2020  stdpc6  2031  equsb1v  2103  ax6dgen  2124  ax13dgen1  2133  ax13dgen3  2135  sbid  2247  exists1  2655  vjust  3447  dfv2  3449  vexOLD  3451  reu6  3687  sbc8g  3750  dfnul2  4290  dfnul2OLD  4292  dfnul3OLD  4293  dfnul4OLD  4294  ab0orv  4343  dfid3  5539  isso2i  5585  relop  5811  iotanul  6479  f1eqcocnv  7252  f1eqcocnvOLD  7253  poxp2  8080  mpoxopoveq  8155  frecseq123  8218  ttrclselem2  9671  dfac2b  10075  konigthlem  10513  hash2prde  14381  hashge2el2difr  14392  pospo  18248  mamulid  21827  mdetdiagid  21986  alexsubALTlem3  23437  trust  23618  isppw2  26501  xmstrkgc  27897  avril1  29470  sa-abvi  31448  wlimeq12  34480  bj-ssbid2  35202  bj-ssbid1  35204  mptsnunlem  35882  ax12eq  37476  elnev  42840  ipo0  42851  ifr0  42852  tratrb  42940  tratrbVD  43265  unirnmapsn  43556  hspmbl  44990  et-equeucl  45233