NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-8 GIF version

Axiom ax-8 1675
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 1682). 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 = zy = z))

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3 setvar x
2 vy . . 3 setvar y
31, 2weq 1643 . 2 wff x = y
4 vz . . . 4 setvar z
51, 4weq 1643 . . 3 wff x = z
62, 4weq 1643 . . 3 wff y = z
75, 6wi 4 . 2 wff (x = zy = z)
83, 7wi 4 1 wff (x = y → (x = zy = z))
Colors of variables: wff setvar class
This axiom is referenced by:  equid  1676  equidOLD  1677  equcomi  1679  equtr  1682  equequ1  1684  equequ1OLD  1685  ax12olem1  1927  ax10lem1  1936  equvini  1987  equveli  1988  aev  1991  ax16i  2046  hbequid  2160  equidqe  2173  aev-o  2182  mo  2226
  Copyright terms: Public domain W3C validator