ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-8 Unicode version

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

Axioms ax-8 1266 through ax-16 1481 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 1481 and ax-17 1280 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 1481 and ax-17 1280 only. (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 1263 . 2
4 vz . . . 4
51, 4weq 1263 . . 3
62, 4weq 1263 . . 3
75, 6wi 4 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hbequid  1276  equidqe  1284  equidqeOLD  1285  equid  1392  equcomi  1394  equtr  1397  equequ1  1400  equvini  1434  equveli  1435  aev  1479  ax16i  1542  mo  1685  ax4  1808  a12lem1  1822  a12study  1824  a12study3  1827
  Copyright terms: Public domain W3C validator