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 1968	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1928	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  nfequid  2016  equcomiv  2017  equcomi  2020  stdpc6  2031  equsb1v  2108  ax6dgen  2128  ax13dgen1  2137  ax13dgen3  2139  sbid  2253  exists1  2744  vjust  3495  vex  3497  vexOLD  3498  reu6  3716  sbc8g  3779  dfnul2  4292  dfnul3  4294  dfid3  5456  isso2i  5502  relop  5715  domepOLD  5788  iotanul  6327  f1eqcocnv  7051  fsplitOLD  7807  mpoxopoveq  7879  ruv  9060  dfac2b  9550  konigthlem  9984  hash2prde  13822  hashge2el2difr  13833  pospo  17577  mamulid  21044  mdetdiagid  21203  alexsubALTlem3  22651  trust  22832  isppw2  25686  xmstrkgc  26666  avril1  28236  sa-abvi  30214  wlimeq12  33101  frecseq123  33114  bj-ssbid2  33990  bj-ssbid1  33992  mptsnunlem  34613  ax12eq  36071  elnev  40763  ipo0  40774  ifr0  40775  tratrb  40863  tratrbVD  41188  unirnmapsn  41470  hspmbl  42905