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

Axiom ax-8 1688
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 1695). 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 1654 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1654 . . 3  wff  x  =  z
62, 4weq 1654 . . 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  1689  equidOLD  1690  equcomi  1692  equtr  1695  equequ1  1697  equequ1OLD  1698  ax12olem1  2006  ax12olem2  2007  ax12olem1OLD  2012  ax10lem1  2023  aev  2048  ax16i  2052  equvini  2084  equviniOLD  2085  equveli  2086  equveliOLD  2087  hbequid  2239  equidqe  2252  aev-o  2261  mo  2305  dtru  4392  axextnd  8468  wl-exeq  26236  wl-aleq  26237  2spotmdisj  28459  a9e2eq  28646  a9e2eqVD  29021  aevwAUX7  29524  equviniNEW7  29529  equveliNEW7  29530  ax16iNEW7  29553  ax7w9AUX7  29662  alcomw9bAUX7  29663
  Copyright terms: Public domain W3C validator