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

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

Axioms ax-8 1387 through ax-16 1644 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 1644 and ax-17 1402 are still valid even when x, y, and z 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 1644 and ax-17 1402 only.

Assertion
Ref Expression
ax-8 (x = y → (x = zy = z))

Detailed syntax breakdown of Axiom ax-8
StepHypRef Expression
1 vx . . 3 set x
2 vy . . 3 set y
31, 2weq 1384 . 2 wff x = y
4 vz . . . 4 set z
51, 4weq 1384 . . 3 wff x = z
62, 4weq 1384 . . 3 wff y = z
75, 6wi 4 . 2 wff (x = zy = z)
83, 7wi 4 1 wff (x = y → (x = zy = z))
Colors of variables: wff set class
This axiom is referenced by:  hbequid  1397  hbequidOLD  1398  a9wa9lem1  1404  a9wa9lem2  1405  a9wa9lem2OLD  1406  equidqe  1419  equidqeOLD  1420  ax4  1423  equid1  1561  equcomi  1564  equtr  1567  equequ1  1570  equvini  1602  equveli  1603  aev  1642  ax16i  1707  a12lem1  1823  a12study  1825  a12study3  1828  mo  1845
  Copyright terms: Public domain W3C validator