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

Axiom ax-7 1798
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 1804). 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 1741 . 2  wff  x  =  y
4 vz . . . 4  setvar  z
51, 4weq 1741 . . 3  wff  x  =  z
62, 4weq 1741 . . 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  1799  equcomi  1801  equtr  1804  equequ1  1806  cbvaev  1825  aev  1951  aevOLD  2068  aevALT  2069  axc16i  2070  equveli  2094  mo3OLD  2259  axext3  2362  dtru  4556  axextnd  8879  2spotmdisj  25189  wl-aetr  30148  wl-exeq  30152  wl-aleq  30153  wl-nfeqfb  30155  ax6e2eq  33670  ax6e2eqVD  34054  bj-aev  34669  bj-dtru  34730  hbequid  35052  equidqe  35065  aev-o  35074
  Copyright terms: Public domain W3C validator