Theorem equid 1926

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, 5-Feb-2018.) (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 1924	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 50	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1877	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1846	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  nfequid  1927  equcomiv  1928  equcomi  1931  stdpc6  1944  ax6dgen  1992  ax13dgen1  2001  ax13dgen3  2003  sbid  2100  exists1  2549  vjust  3174  vex  3176  reu6  3362  nfccdeq  3400  sbc8g  3410  dfnul3  3877  rab0OLD  3910  int0OLD  4426  dfid3  4954  isso2i  4991  relop  5194  f1eqcocnv  6456  fsplit  7169  mpt2xopoveq  7232  ruv  8390  dfac2  8836  konigthlem  9269  hash2prde  13109  hashge2el2difr  13118  pospo  16796  mamulid  20066  mdetdiagid  20225  alexsubALTlem3  21663  trust  21843  isppw2  24641  xmstrkgc  25566  nbgranself  25963  usgrasscusgra  26011  rusgrasn  26472  avril1  26711  foo3  28686  domep  30942  wlimeq12  31009  bj-ssbid2  31834  bj-ssbid1  31836  bj-vjust  31974  mptsnunlem  32361  ax12eq  33244  elnev  37661  ipo0  37674  ifr0  37675  tratrb  37767  tratrbVD  38119  unirnmapsn  38401  hspmbl  39519