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

Axiom ax-8 1687
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 1694). 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 1653 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1653 . . 3  wff  x  =  z
62, 4weq 1653 . . 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  1688  equidOLD  1689  equcomi  1691  equtr  1694  equequ1  1696  equequ1OLD  1697  ax12olem1  2005  ax12olem2  2006  ax12olem1OLD  2011  ax10lem1  2022  aev  2047  equvini  2079  equviniOLD  2080  equveli  2081  equveliOLD  2082  ax16i  2130  hbequid  2236  equidqe  2249  aev-o  2258  mo  2302  dtru  4382  axextnd  8458  wl-exeq  26226  wl-aleq  26227  2spotmdisj  28394  a9e2eq  28581  a9e2eqVD  28956  aevwAUX7  29459  equviniNEW7  29464  equveliNEW7  29465  ax16iNEW7  29488  ax7w9AUX7  29597  alcomw9bAUX7  29598
  Copyright terms: Public domain W3C validator