Theorem equid 2019

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 2017	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1972	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1932	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 1911  ax-6 1970  ax-7 2015

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

This theorem is referenced by:  nfequid  2020  equcomiv  2021  equcomi  2024  stdpc6  2035  equsb1v  2109  ax6dgen  2129  ax13dgen1  2138  ax13dgen3  2140  sbid  2254  exists1  2723  vjust  3442  vex  3444  vexOLD  3445  reu6  3665  sbc8g  3728  dfnul2  4245  dfnul3  4246  abf  4310  dfid3  5427  isso2i  5472  relop  5685  domepOLD  5758  iotanul  6302  f1eqcocnv  7035  f1eqcocnvOLD  7036  fsplitOLD  7796  mpoxopoveq  7868  ruv  9050  dfac2b  9541  konigthlem  9979  hash2prde  13824  hashge2el2difr  13835  pospo  17575  mamulid  21046  mdetdiagid  21205  alexsubALTlem3  22654  trust  22835  isppw2  25700  xmstrkgc  26680  avril1  28248  sa-abvi  30226  wlimeq12  33219  frecseq123  33232  bj-ssbid2  34108  bj-ssbid1  34110  mptsnunlem  34755  ax12eq  36237  elnev  41142  ipo0  41153  ifr0  41154  tratrb  41242  tratrbVD  41567  unirnmapsn  41843  hspmbl  43268