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

Axiom ax-8 1683
 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 1690). 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 , , and 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, 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 1650 . 2
4 vz . . . 4
51, 4weq 1650 . . 3
62, 4weq 1650 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  equid  1684  equidOLD  1685  equcomi  1687  equtr  1690  equequ1  1692  equequ1OLD  1693  ax12olem1  1972  ax12olem2  1973  ax12olem1OLD  1977  ax10lem1  1988  aev  2011  equvini  2040  equviniOLD  2041  equveli  2042  equveliOLD  2043  ax16i  2095  hbequid  2210  equidqe  2223  aev-o  2232  mo  2276  dtru  4350  axextnd  8422  2spotmdisj  28171  a9e2eq  28355  a9e2eqVD  28728  aevwAUX7  29226  equviniNEW7  29231  equveliNEW7  29232  ax16iNEW7  29255  ax7w9AUX7  29360  alcomw9bAUX7  29361
 Copyright terms: Public domain W3C validator