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

Axiom ax-7 1790
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 1796). 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, 10-Jan-1993.)

Assertion
Ref Expression
ax-7

Detailed syntax breakdown of Axiom ax-7
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1733 . 2
4 vz . . . 4
51, 4weq 1733 . . 3
62, 4weq 1733 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  equid  1791  equcomi  1793  equtr  1796  equequ1  1798  cbvaev  1817  aev  1943  aevOLD  2062  aevALT  2063  axc16i  2064  equveli  2088  equveliOLD  2089  hbequid  2239  equidqe  2252  aev-o  2261  mo3OLD  2324  axext3  2437  dtru  4643  axextnd  8987  2spotmdisj  25068  wl-aetr  29983  wl-exeq  29987  wl-aleq  29988  wl-nfeqfb  29990  ax6e2eq  33330  ax6e2eqVD  33707  bj-aev  34322  bj-dtru  34383
  Copyright terms: Public domain W3C validator