Theorem equid 2007

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003

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

This theorem is referenced by:  nfequid  2008  equcomiv  2009  equcomi  2012  stdpc6  2023  equsb1v  2101  ax6dgen  2124  ax13dgen1  2133  ax13dgen3  2135  sbid  2251  exists1  2657  vjust  3478  dfv2  3480  reu6  3735  sbc8g  3799  dfnul2  4342  ab0orv  4389  dfid3  5580  isso2i  5628  relop  5859  iotanul  6537  f1eqcocnv  7315  poxp2  8162  mpoxopoveq  8238  frecseq123  8301  ttrclselem2  9758  dfac2b  10163  konigthlem  10600  hash2prde  14496  hashge2el2difr  14507  pospo  18392  mamulid  22445  mdetdiagid  22604  alexsubALTlem3  24055  trust  24236  isppw2  27155  xmstrkgc  28897  avril1  30474  sa-abvi  32454  wlimeq12  35761  bj-ssbid2  36605  bj-ssbid1  36607  mptsnunlem  37281  ax12eq  38884  elnev  44400  ipo0  44411  ifr0  44412  tratrb  44500  tratrbVD  44825  unirnmapsn  45114  hspmbl  46542  et-equeucl  46785