Theorem equid 2116

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112

This theorem depends on definitions:  df-bi 199  df-ex 1879

This theorem is referenced by:  nfequid  2117  equcomiv  2118  equcomi  2121  stdpc6  2132  ax6dgen  2179  ax13dgen1  2188  ax13dgen3  2190  sbid  2289  exists1  2743  vjust  3415  vex  3417  reu6  3620  nfccdeq  3660  sbc8g  3670  dfnul3  4147  dfid3  5251  isso2i  5295  relop  5505  iotanul  6101  f1eqcocnv  6811  fsplit  7546  mpt2xopoveq  7610  ruv  8776  dfac2b  9266  dfac2OLD  9268  konigthlem  9705  hash2prde  13541  hashge2el2difr  13552  pospo  17326  mamulid  20614  mdetdiagid  20774  alexsubALTlem3  22223  trust  22403  isppw2  25254  xmstrkgc  26185  avril1  27866  sa-abvi  29846  domep  32225  wlimeq12  32292  frecseq123  32305  bj-ssbid2  33174  bj-ssbid1  33176  bj-vjust  33304  mptsnunlem  33724  ax12eq  35009  elnev  39471  ipo0  39484  ifr0  39485  tratrb  39573  tratrbVD  39908  unirnmapsn  40205  hspmbl  41630