NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-8 Unicode version

Axiom ax-8 1402
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 1529). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105.

Axioms ax-8 1402 through ax-16 1606 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 1606 and ax-17 1413 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 1606 and ax-17 1413 only.

Assertion
Ref Expression
ax-8

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3
2 vy . . 3
31, 2weq 1399 . 2
4 vz . . . 4
51, 4weq 1399 . . 3
62, 4weq 1399 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hbequid  1408  a9wa9lem1  1415  a9wa9lem2  1416  equidqe  1425  ax4  1428  equid1  1524  equcomi  1526  equtr  1529  equequ1  1532  equvini  1564  equveli  1565  aev  1604  ax16i  1669  a12lem1  1785  a12study  1787  a12study3  1790  mo  1807
  Copyright terms: Public domain W3C validator