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 (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 , , and 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

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1620 . 2
4 vz . . . 4
51, 4weq 1620 . . 3
62, 4weq 1620 . . 3
75, 6wi 6 . 2
83, 7wi 6 1
 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  a12lem1  27819  a12study10  27825  a12study10n  27826  ax9lem1  27829  ax9lem2  27830  ax9lem6  27834  ax9lem14  27842  ax9lem15  27843  ax9vax9  27847
 Copyright terms: Public domain W3C validator