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

Axiom ax-7 1862
Description: Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. It states that equality is right-Euclidean (this is similar, but not identical, to being transitive, which is proved as equtr 1876). 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."

We prove in ax7 1871 that this axiom can be recovered from its weakened version ax7v 1863 where  x and  y are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1862 should be ax7v 1863. See the comment of ax7v 1863 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1871 instead. (New usage is discouraged.)

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 1802 . 2  wff  x  =  y
4 vz . . . 4  setvar  z
51, 4weq 1802 . . 3  wff  x  =  z
62, 4weq 1802 . . 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:  ax7v  1863
  Copyright terms: Public domain W3C validator