Axiom ax-8 966

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

Axioms ax-8 966 through ax-16 1212 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 1212 and ax-17 973 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 1212 and ax-17 973 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 957	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 957	. . 3 class y
5	2, 4	wceq 958	. 2 wff x = y
6		vz	. . . . 5 set z
7	6	cv 957	. . . 4 class z
8	2, 7	wceq 958	. . 3 wff x = z
9	4, 7	wceq 958	. . 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:  ax4 974  equcomi 1130  equtr 1133  equequ1 1136  equvini 1170  aev 1210  equid1 1271  ax16i 1272  a12lem1 1378  a12study 1380  mo 1395  dtruALT 2755  axextnd 4962

Copyright terms: Public domain