Theorem equid 2047

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 2045	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 53	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 2004	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1966	1 ⊢ 𝑥 = 𝑥

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  nfequid  2048  equcomiv  2049  equcomi  2052  stdpc6  2063  equsb1v  2144  ax6dgen  2167  ax13dgen1  2176  ax13dgen3  2178  sbid  2294  exists1  2688  vjust  3455  dfv2  3457  reu6  3687  sbc8g  3750  dfnul2  4284  dfid3  5556  isso2i  5603  relop  5838  iotanul  6545  f1eqcocnv  7340  poxp2  8197  mpoxopoveq  8274  frecseq123  8338  ttrclselem2  9764  dfac2b  10248  konigthlem  10692  hash2prde  14656  hashge2el2difr  14667  pospo  18567  mamulid  22811  mdetdiagid  22970  alexsubALTlem3  24423  trust  24603  isppw2  27499  xmstrkgc  29520  avril1  31121  sa-abvi  33144  reu6f  35820  wlimeq12  36796  bj-dfnul2  37655  bj-ssbid2  37776  bj-ssbid1  37778  mptsnunlem  38529  ax12eq  40264  elnev  45681  ipo0  45692  ifr0  45693  tratrb  45779  tratrbVD  46103  unirnmapsn  46500  hspmbl  47912  et-equeucl  48155  nprmmul3  48884  resipos  50420