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 1926 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 1926 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 1926 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  1879  equveli  1880  aev  1923  aev-o  1924  ax16i  1994  mo  2135  dtru  4095  axextnd  8093  a9e2eq  27016  a9e2eqVD  27373  equidK  27792  equcomiK  27793  equequ1K  27794  equequ2K  27795  ax12o10lem1X  27833  ax12o10lem2X  27834  equvinvK  27861  ax12olem21K  27872  ax12olem21X  27873  ax12olem22K  27875  ax10lem16X  27886  ax10lem20X  27890  a12lem1  27931  a12study10  27937  a12study10n  27938  ax9lem1  27941  ax9lem2  27942  ax9lem6  27946  ax9lem14  27954  ax9lem15  27955  ax9vax9  27959
  Copyright terms: Public domain W3C validator