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

Axiom ax-7 1697
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 1703). 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 1663 . 2
4 vz . . . 4
51, 4weq 1663 . . 3
62, 4weq 1663 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  equid  1698  equcomi  1700  equtr  1703  equequ1  1705  axc9lem1OLD  2009  axc11nlem1  2019  aev  2045  aevALT  2046  axc16i  2049  equviniOLD  2084  equveli  2085  equveliOLD  2086  hbequid  2262  equidqe  2275  aev-o  2284  mo3  2336  moOLD  2344  dtru  4490  axextnd  8580  wl-exeq  27079  wl-aleq  27080  2spotmdisj  29520  a6e2eq  29835  a6e2eqVD  30212  aevwAUX11  30797  equviniNEW11  30802  equveliNEW11  30803  axc16iNEW11  30826  ax11w9AUX11  30934  alcomw9bAUX11  30935
  Copyright terms: Public domain W3C validator