Axiom ax-8 1594

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

Axioms ax-8 1594 through ax-16 1854 are the axioms having to do with equality, substitution, and logical properties of our binary predicate e. (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1854 and ax-17 1605 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 1854 and ax-17 1605 only.

Assertion

Ref	Expression
ax-8	|- (x = y -> (x = z -> y = z))

Detailed syntax breakdown of Axiom ax-8

Step	Hyp	Ref	Expression
1		vx	. . . 4 set x
2	1	cv 1585	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 1585	. . 3 class y
5	2, 4	wceq 1586	. 2 wff x = y
6		vz	. . . . 5 set z
7	6	cv 1585	. . . 4 class z
8	2, 7	wceq 1586	. . 3 wff x = z
9	4, 7	wceq 1586	. . 3 wff y = z
10	8, 9	wi 3	. 2 wff (x = z -> y = z)
11	5, 10	wi 3	1 wff (x = y -> (x = z -> y = z))

This axiom is referenced by:  hbequid 1601  equidqe 1602  ax4 1607  equcomi 1769  equtr 1772  equequ1 1775  equvini 1811  equveli 1812  aev 1852  equid1 1916  ax16i 1917  a12lem1 2031  a12study 2033  a12study3 2036  mo 2053  dtru 3662  axextnd 6461

Copyright terms: Public domain