|Intuitionistic Logic Explorer||
|Mirrors > Home > ILE Home > Th. List > ax-8||GIF version|
|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.
|ax-8||⊢ (x = y → (x = z → y = z))|
|1||vx||. . 3 set x|
|2||vy||. . 3 set y|
|3||1, 2||weq 1384||. 2 wff x = y|
|4||vz||. . . 4 set z|
|5||1, 4||weq 1384||. . 3 wff x = z|
|6||2, 4||weq 1384||. . 3 wff y = z|
|7||5, 6||wi 4||. 2 wff (x = z → y = z)|
|8||3, 7||wi 4||1 wff (x = y → (x = z → y = 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|