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

Axiom ax-7 1705
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 1711). 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-7

Detailed syntax breakdown of Axiom ax-7
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1671 . 2
4 vz . . . 4
51, 4weq 1671 . . 3
62, 4weq 1671 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  equid  1706  equcomi  1708  equtr  1711  equequ1  1713  axc9lem1OLD  2017  axc11nlem1  2027  aev  2053  aevALT  2054  axc16i  2057  equviniOLD  2092  equveli  2093  equveliOLD  2094  hbequid  2270  equidqe  2283  aev-o  2292  mo3  2344  moOLD  2352  dtru  4506  axextnd  8637  wl-exeq  27588  wl-aleq  27589  2spotmdisj  29842  a6e2eq  30112  a6e2eqVD  30489  aevwAUX11  31074  equviniNEW11  31079  equveliNEW11  31080  axc16iNEW11  31103  ax11w9AUX11  31211  alcomw9bAUX11  31212
  Copyright terms: Public domain W3C validator