Theorem equid 2014

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

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

This theorem is referenced by:  nfequid  2015  equcomiv  2016  equcomi  2019  stdpc6  2030  equsb1v  2111  ax6dgen  2134  ax13dgen1  2143  ax13dgen3  2145  sbid  2263  exists1  2662  vjust  3431  dfv2  3433  reu6  3673  sbc8g  3737  dfnul2  4277  dfid3  5523  isso2i  5570  relop  5800  iotanul  6473  f1eqcocnv  7250  poxp2  8087  mpoxopoveq  8163  frecseq123  8226  ttrclselem2  9641  dfac2b  10047  konigthlem  10485  hash2prde  14426  hashge2el2difr  14437  pospo  18303  mamulid  22419  mdetdiagid  22578  alexsubALTlem3  24027  trust  24207  isppw2  27095  xmstrkgc  28971  avril1  30551  sa-abvi  32532  wlimeq12  36018  bj-dfnul2  36854  bj-ssbid2  36975  bj-ssbid1  36977  mptsnunlem  37671  ax12eq  39404  elnev  44885  ipo0  44896  ifr0  44897  tratrb  44984  tratrbVD  45308  unirnmapsn  45664  hspmbl  47078  et-equeucl  47321  nprmmul3  48004  resipos  49465