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

Theorem equid 1791
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, 5-Feb-2018.)
Assertion
Ref Expression
equid

Proof of Theorem equid
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax6ev 1749 . . 3
2 ax-7 1790 . . . 4
32pm2.43i 47 . . 3
41, 3eximii 1658 . 2
5 ax5e 1706 . 2
64, 5ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  E.wex 1612
This theorem is referenced by:  nfequid  1792  equcomi  1793  stdpc6  1800  ax6dgen  1824  ax13dgen1  1833  ax13dgen3  1835  sbid  1996  ax12eq  2271  exists1  2388  vjust  3110  vex  3112  reu6  3288  nfccdeq  3325  sbc8g  3335  dfnul3  3787  rab0  3806  int0  4300  reusv5OLD  4662  reusv7OLD  4664  dfid3  4801  isso2i  4837  relop  5158  f1eqcocnv  6204  fsplit  6905  mpt2xopoveq  6966  ruv  8048  dfac2  8532  konigthlem  8964  hash2prde  12516  pospo  15603  mamulid  18943  mdetdiagid  19102  alexsubALTlem3  20549  trust  20732  isppw2  23389  xmstrkgc  24189  nbgranself  24434  usgrasscusgra  24483  rusgrasn  24945  avril1  25171  mathbox  27361  foo3  27362  domep  29225  wlimeq12  29375  elnev  31345  ipo0  31358  ifr0  31359  tratrb  33307  tratrbVD  33661  bj-vjust  34372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator