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

Axiom ax-8 1690
Description: Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. This is similar to, but not quite, a transitive law for equality (proved later as equtr 1697). This axiom scheme is a sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose general form cannot be represented with our notation. Also appears as Axiom C7 of [Monk2] p. 105 and Axiom Scheme C8' in [Megill] p. 448 (p. 16 of the preprint).

The equality symbol was invented in 1527 by Robert Recorde. He chose a pair of parallel lines of the same length because "noe .2. thynges, can be moare equalle."

Note that this axiom is still valid even when any two or all three of , , and are replaced with the same variable since they do not have any distinct variable (Metamath's $d) restrictions. Because of this, we say that these three variables are "bundled" (a term coined by Raph Levien). (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-8

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1655 . 2
4 vz . . . 4
51, 4weq 1655 . . 3
62, 4weq 1655 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  equid  1691  equidOLD  1692  equcomi  1694  equtr  1697  equequ1  1699  equequ1OLD  1700  ax12olem1  2009  ax12olem2  2010  ax12olem1OLD  2015  ax10lem1  2026  aev  2051  ax16i  2055  equvini  2087  equviniOLD  2088  equveli  2089  equveliOLD  2090  hbequid  2244  equidqe  2257  aev-o  2266  mo  2310  dtru  4429  axextnd  8517  wl-exeq  26338  wl-aleq  26339  2spotmdisj  28695  a9e2eq  28883  a9e2eqVD  29260  aevwAUX7  29763  equviniNEW7  29768  equveliNEW7  29769  ax16iNEW7  29792  ax7w9AUX7  29901  alcomw9bAUX7  29902
  Copyright terms: Public domain W3C validator