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

Axiom ax-8 1623
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 1826). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105.

This is our first use of the equality symbol, 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."

Axioms ax-8 1623 through ax-16 1927 are the axioms having to do with equality, substitution, and logical properties of our binary predicate  e. (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1927 and ax-17 1628 are still valid even when  x,  y, and  z are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 1927 and ax-17 1628 only. (Contributed by NM, 5-Aug-1993.)

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

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3  set  x
2 vy . . 3  set  y
31, 2weq 1620 . 2  wff  x  =  y
4 vz . . . 4  set  z
51, 4weq 1620 . . 3  wff  x  =  z
62, 4weq 1620 . . 3  wff  y  =  z
75, 6wi 6 . 2  wff  ( x  =  z  ->  y  =  z )
83, 7wi 6 1  wff  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
Colors of variables: wff set class
This axiom is referenced by:  ax12o10lem1  1635  ax12o10lem2  1636  ax12olem21  1655  ax10lem16  1665  ax10lem20  1669  equidqe  1686  hbequid  1687  ax4  1691  equid1  1820  equcomi  1822  equcomi-o  1823  equtr  1826  equequ1  1829  equvini  1880  equveli  1881  aev  1924  aev-o  1925  ax16i  1995  mo  2138  dtru  4139  axextnd  8146  a9e2eq  27339  a9e2eqVD  27696  equidK  28115  equcomiK  28116  equequ1K  28117  equequ2K  28118  ax12o10lem1X  28162  ax12o10lem2X  28163  equvinvK  28190  ax12olem21K  28201  ax12olem21X  28202  ax12olem22K  28204  ax10lem16X  28215  ax10lem20X  28219  a12lem1  28260  a12study10  28266  a12study10n  28267  ax9lem1  28270  ax9lem2  28271  ax9lem6  28275  ax9lem14  28283  ax9lem15  28284  ax9vax9  28288
  Copyright terms: Public domain W3C validator