Theorem equid 2015

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 2013	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥)
3		ax6ev 1973	. 2 ⊢ ∃𝑦 𝑦 = 𝑥
4	2, 3	exlimiiv 1934	1 ⊢ 𝑥 = 𝑥

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  nfequid  2016  equcomiv  2017  equcomi  2020  stdpc6  2031  equsb1v  2103  ax6dgen  2124  ax13dgen1  2133  ax13dgen3  2135  sbid  2248  exists1  2662  vjust  3433  dfv2  3435  vexOLD  3437  reu6  3661  sbc8g  3724  dfnul2  4259  dfnul2OLD  4261  dfnul3OLD  4262  dfnul4OLD  4263  ab0orv  4312  dfid3  5492  isso2i  5538  relop  5759  domepOLD  5833  iotanul  6411  f1eqcocnv  7173  f1eqcocnvOLD  7174  fsplitOLD  7958  mpoxopoveq  8035  frecseq123  8098  ttrclselem2  9484  dfac2b  9886  konigthlem  10324  hash2prde  14184  hashge2el2difr  14195  pospo  18063  mamulid  21590  mdetdiagid  21749  alexsubALTlem3  23200  trust  23381  isppw2  26264  xmstrkgc  27253  avril1  28827  sa-abvi  30805  poxp2  33790  wlimeq12  33813  bj-ssbid2  34843  bj-ssbid1  34845  mptsnunlem  35509  ax12eq  36955  elnev  42056  ipo0  42067  ifr0  42068  tratrb  42156  tratrbVD  42481  unirnmapsn  42754  hspmbl  44167