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

Axiom ax-7 1843
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 1850). 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, 10-Jan-1993.)

Assertion
Ref Expression
ax-7  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )

Detailed syntax breakdown of Axiom ax-7
StepHypRef Expression
1 vx . . 3  setvar  x
2 vy . . 3  setvar  y
31, 2weq 1784 . 2  wff  x  =  y
4 vz . . . 4  setvar  z
51, 4weq 1784 . . 3  wff  x  =  z
62, 4weq 1784 . . 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 setvar class
This axiom is referenced by:  equid  1844  equidOLD  1845  equcomi  1847  equtr  1850  equequ1  1852  cbvaev  1871  aev  2003  aevOLD  2121  aevALT  2122  axc16i  2123  equveli  2147  axext3  2403  dtru  4615  axextnd  9023  2spotmdisj  25794  bj-aev  31321  bj-dtru  31382  bj-mo3OLD  31417  wl-aetr  31827  wl-exeq  31831  wl-aleq  31832  wl-nfeqfb  31834  hbequid  32449  equidqe  32462  aev-o  32471  ax6e2eq  36894  ax6e2eqVD  37277
  Copyright terms: Public domain W3C validator