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

Axiom ax-8 1682
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 1689). 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  x,  y, and  z 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  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3  set  x
2 vy . . 3  set  y
31, 2weq 1650 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1650 . . 3  wff  x  =  z
62, 4weq 1650 . . 3  wff  y  =  z
75, 6wi 4 . 2  wff  ( x  =  z  ->  y  =  z )
83, 7wi 4 1  wff  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
Colors of variables: wff set class
This axiom is referenced by:  equid  1683  equidOLD  1684  equcomi  1686  equtr  1689  equequ1  1691  equequ1OLD  1692  ax12olem1  1962  ax12olem2  1963  ax12olem1OLD  1967  ax10lem1  1980  equvini  2024  equveli  2025  aev  2027  ax16i  2080  hbequid  2195  equidqe  2208  aev-o  2217  mo  2261  dtru  4332  axextnd  8400  a9e2eq  27988  a9e2eqVD  28361  aevwAUX7  28859  equviniNEW7  28864  equveliNEW7  28865  ax16iNEW7  28888  ax7w9AUX7  28993  alcomw9bAUX7  28994
  Copyright terms: Public domain W3C validator