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

Axiom ax-7 1841
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 1848). 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 1783 . 2  wff  x  =  y
4 vz . . . 4  setvar  z
51, 4weq 1783 . . 3  wff  x  =  z
62, 4weq 1783 . . 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  1842  equidOLD  1843  equcomi  1845  equtr  1848  equequ1  1850  cbvaev  1869  aev  2001  aevOLD  2118  aevALT  2119  axc16i  2120  equveli  2144  axext3  2409  dtru  4616  axextnd  9014  2spotmdisj  25641  bj-aev  31102  bj-dtru  31163  bj-mo3OLD  31198  wl-aetr  31570  wl-exeq  31574  wl-aleq  31575  wl-nfeqfb  31577  hbequid  32188  equidqe  32201  aev-o  32210  ax6e2eq  36560  ax6e2eqVD  36943
  Copyright terms: Public domain W3C validator