Theorem equid 2012

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  nfequid  2013  equcomiv  2014  equcomi  2017  stdpc6  2028  equsb1v  2106  ax6dgen  2129  ax13dgen1  2138  ax13dgen3  2140  sbid  2256  exists1  2654  vjust  3437  dfv2  3439  reu6  3686  sbc8g  3750  dfnul2  4287  ab0orv  4334  dfid3  5517  isso2i  5564  relop  5793  iotanul  6462  f1eqcocnv  7238  poxp2  8076  mpoxopoveq  8152  frecseq123  8215  ttrclselem2  9622  dfac2b  10025  konigthlem  10462  hash2prde  14377  hashge2el2difr  14388  pospo  18249  mamulid  22326  mdetdiagid  22485  alexsubALTlem3  23934  trust  24115  isppw2  27023  xmstrkgc  28831  avril1  30407  sa-abvi  32387  wlimeq12  35793  bj-ssbid2  36636  bj-ssbid1  36638  mptsnunlem  37312  ax12eq  38920  elnev  44411  ipo0  44422  ifr0  44423  tratrb  44510  tratrbVD  44834  unirnmapsn  45192  hspmbl  46610  et-equeucl  46853  resipos  48959