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

Axiom ax-7 1734
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 1740). 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 1700 . 2  wff  x  =  y
4 vz . . . 4  setvar  z
51, 4weq 1700 . . 3  wff  x  =  z
62, 4weq 1700 . . 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  1735  equcomi  1737  equtr  1740  equequ1  1742  cbvaev  1761  aev  1885  aevOLD  2030  aevALT  2031  axc16i  2032  equveli  2056  equveliOLD  2057  hbequid  2227  equidqe  2240  aev-o  2249  mo3OLD  2316  moOLD  2322  axext3  2442  dtru  4633  axextnd  8957  2spotmdisj  24733  wl-aetr  29548  wl-exeq  29552  wl-aleq  29553  wl-nfeqfb  29555  ax6e2eq  32287  ax6e2eqVD  32664  bj-aev  33280  bj-dtru  33341
  Copyright terms: Public domain W3C validator