Theorem equid 2012

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  nfequid  2013  equcomiv  2014  equcomi  2017  stdpc6  2028  equsb1v  2106  ax6dgen  2129  ax13dgen1  2138  ax13dgen3  2140  sbid  2256  exists1  2654  vjust  3448  dfv2  3450  reu6  3697  sbc8g  3761  dfnul2  4299  ab0orv  4346  dfid3  5536  isso2i  5583  relop  5814  iotanul  6489  f1eqcocnv  7276  poxp2  8122  mpoxopoveq  8198  frecseq123  8261  ttrclselem2  9679  dfac2b  10084  konigthlem  10521  hash2prde  14435  hashge2el2difr  14446  pospo  18304  mamulid  22328  mdetdiagid  22487  alexsubALTlem3  23936  trust  24117  isppw2  27025  xmstrkgc  28813  avril1  30392  sa-abvi  32372  wlimeq12  35807  bj-ssbid2  36650  bj-ssbid1  36652  mptsnunlem  37326  ax12eq  38934  elnev  44427  ipo0  44438  ifr0  44439  tratrb  44526  tratrbVD  44850  unirnmapsn  45208  hspmbl  46627  et-equeucl  46870  resipos  48963