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

Axiom ax-8 1661
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 1671). 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 1633 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1633 . . 3  wff  x  =  z
62, 4weq 1633 . . 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  1662  equcomi  1664  equequ1  1667  equequ1OLD  1668  equtr  1671  ax12olem1  1880  ax10lem1  1889  equvini  1940  equveli  1941  aev  1944  ax16i  1999  hbequid  2112  equidqe  2125  aev-o  2134  mo  2178  dtru  4217  axextnd  8229  a9e2eq  28622  a9e2eqVD  28999  aevwAUX7  29497  equviniNEW7  29502  equveliNEW7  29503  ax16iNEW7  29526  ax7w9AUX7  29630  alcomw9bAUX7  29631  a12lem1  29752  a12study10  29758  a12study10n  29759  ax9lem1  29762  ax9lem2  29763  ax9lem6  29767  ax9lem14  29775  ax9lem15  29776  ax9vax9  29780
  Copyright terms: Public domain W3C validator