Axiom ax-8 964

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

Axioms ax-8 964 through ax-16 1210 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 1210 and ax-17 971 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 1210 and ax-17 971 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 955	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 955	. . 3 class y
5	2, 4	wceq 956	. 2 wff x = y
6		vz	. . . . 5 set z
7	6	cv 955	. . . 4 class z
8	2, 7	wceq 956	. . 3 wff x = z
9	4, 7	wceq 956	. . 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 972  equcomi 1128  equtr 1131  equequ1 1134  equvini 1168  aev 1208  equid1 1269  ax16i 1270  a12lem1 1376  a12study 1378  mo 1393  dtruALT 2748  axextnd 4943

Copyright terms: Public domain