Theorem equid 2014

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  nfequid  2015  equcomiv  2016  equcomi  2019  stdpc6  2030  equsb1v  2111  ax6dgen  2134  ax13dgen1  2143  ax13dgen3  2145  sbid  2263  exists1  2661  vjust  3430  dfv2  3432  reu6  3672  sbc8g  3736  dfnul2  4276  dfid3  5529  isso2i  5576  relop  5805  iotanul  6478  f1eqcocnv  7256  poxp2  8093  mpoxopoveq  8169  frecseq123  8232  ttrclselem2  9647  dfac2b  10053  konigthlem  10491  hash2prde  14432  hashge2el2difr  14443  pospo  18309  mamulid  22406  mdetdiagid  22565  alexsubALTlem3  24014  trust  24194  isppw2  27078  xmstrkgc  28954  avril1  30533  sa-abvi  32514  wlimeq12  35999  bj-dfnul2  36835  bj-ssbid2  36956  bj-ssbid1  36958  mptsnunlem  37654  ax12eq  39387  elnev  44864  ipo0  44875  ifr0  44876  tratrb  44963  tratrbVD  45287  unirnmapsn  45643  hspmbl  47057  et-equeucl  47300  nprmmul3  47989  resipos  49450