Axiom ax-8 1101

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

Axioms ax-8 1101 through ax-16 1194 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 1194 and ax-17 1190 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 1194 and ax-17 1190 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 1098	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 1098	. . 3 class y
5	2, 4	wceq 1099	. 2 wff x = y
6		vz	. . . . 5 set z
7	6	cv 1098	. . . 4 class z
8	2, 7	wceq 1099	. . 3 wff x = z
9	4, 7	wceq 1099	. . 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:  equcomi 1115  equtr 1118  equequ1 1121  equvini 1151  aev 1192  equid1 1253  a12lem1 1353  a12study 1355  mo 1370  dtruALT 2716  axextnd 4866

Copyright terms: Public domain