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

Axiom ax-8 1646
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 1655). 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 1626 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1626 . . 3  wff  x  =  z
62, 4weq 1626 . . 3  wff  y  =  z
75, 6wi 6 . 2  wff  ( x  =  z  ->  y  =  z )
83, 7wi 6 1  wff  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
Colors of variables: wff set class
This axiom is referenced by:  equid  1647  equcomi  1649  equequ1  1651  equtr  1655  ax12olem1  1872  ax10lem1  1880  equvini  1932  equveli  1933  aev  1936  ax16i  1944  hbequid  2103  equidqe  2116  aev-o  2125  mo  2168  dtru  4202  axextnd  8210  a9e2eq  27596  a9e2eqVD  27953  a12lem1  28399  a12study10  28405  a12study10n  28406  ax9lem1  28409  ax9lem2  28410  ax9lem6  28414  ax9lem14  28422  ax9lem15  28423  ax9vax9  28427
  Copyright terms: Public domain W3C validator