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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  nfequid  2020  equcomiv  2021  equcomi  2024  stdpc6  2035  equsb1v  2116  ax6dgen  2139  ax13dgen1  2148  ax13dgen3  2150  sbid  2267  exists1  2664  vjust  3432  dfv2  3434  reu6  3667  sbc8g  3731  dfnul2  4264  dfid3  5516  isso2i  5563  relop  5792  iotanul  6465  f1eqcocnv  7245  poxp2  8083  mpoxopoveq  8159  frecseq123  8222  ttrclselem2  9638  dfac2b  10044  konigthlem  10482  hash2prde  14423  hashge2el2difr  14434  pospo  18300  mamulid  22424  mdetdiagid  22583  alexsubALTlem3  24032  trust  24212  isppw2  27096  xmstrkgc  28972  avril1  30551  sa-abvi  32532  wlimeq12  36045  bj-dfnul2  36881  bj-ssbid2  37002  bj-ssbid1  37004  mptsnunlem  37700  ax12eq  39433  elnev  44881  ipo0  44892  ifr0  44893  tratrb  44980  tratrbVD  45304  unirnmapsn  45659  hspmbl  47072  et-equeucl  47315  nprmmul3  48004  resipos  49465