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

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

Axioms ax-8 1305 through ax-16 1523 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 1523 and ax-17 1319 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 1523 and ax-17 1319 only. (Contributed by NM, 5-Aug-1993.)

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 1302 . 2 wff x = y
4 vz . . . 4 set z
51, 4weq 1302 . . 3 wff x = z
62, 4weq 1302 . . 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  1315  equidqe  1323  equidqeOLD  1324  ax4  1326  equid1  1440  equcomi  1443  equtr  1446  equequ1  1449  equvini  1481  equveli  1482  aev  1521  ax16i  1586  mo  1706  a12lem1  1798  a12study  1800  a12study3  1803
  Copyright terms: Public domain W3C validator