MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equid Structured version   Visualization version   GIF version

Theorem equid 2010
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.
StepHypRef Expression
1 ax7v1 2008 . . 3 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
21pm2.43i 52 . 2 (𝑦 = 𝑥𝑥 = 𝑥)
3 ax6ev 1963 . 2 𝑦 𝑦 = 𝑥
42, 3exlimiiv 1923 1 𝑥 = 𝑥
Colors of variables: wff setvar class
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  nfequid  2011  equcomiv  2012  equcomi  2015  stdpc6  2026  equsb1v  2103  ax6dgen  2123  ax13dgen1  2132  ax13dgen3  2134  sbid  2247  exists1  2741  vjust  3493  vex  3495  vexOLD  3496  reu6  3714  sbc8g  3777  dfnul2  4290  dfnul3  4292  dfid3  5455  isso2i  5501  relop  5714  domepOLD  5787  iotanul  6326  f1eqcocnv  7048  fsplitOLD  7802  mpoxopoveq  7874  ruv  9054  dfac2b  9544  konigthlem  9978  hash2prde  13816  hashge2el2difr  13827  pospo  17571  mamulid  20978  mdetdiagid  21137  alexsubALTlem3  22585  trust  22765  isppw2  25619  xmstrkgc  26599  avril1  28169  sa-abvi  30147  wlimeq12  33003  frecseq123  33016  bj-ssbid2  33892  bj-ssbid1  33894  mptsnunlem  34501  ax12eq  35957  elnev  40647  ipo0  40658  ifr0  40659  tratrb  40747  tratrbVD  41072  unirnmapsn  41353  hspmbl  42788
  Copyright terms: Public domain W3C validator