Axiom ax-8 1144

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

Axioms ax-8 1144 through ax-16 1418 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 1418 and ax-17 1155 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 1418 and ax-17 1155 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 1135	. . 3 class x
3		vy	. . . 4 set y
4	3	cv 1135	. . 3 class y
5	2, 4	wceq 1136	. 2 wff x = y
6		vz	. . . . 5 set z
7	6	cv 1135	. . . 4 class z
8	2, 7	wceq 1136	. . 3 wff x = z
9	4, 7	wceq 1136	. . 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 1151  equidqe 1152  ax4 1156  equcomi 1325  equtr 1328  equequ1 1332  equvini 1369  equviniOLD 1370  aev 1415  aevOLD 1416  equid1 1484  ax16i 1485  a12lem1 1605  a12study 1607  mo 1625  dtru 3313  axextnd 5891

Copyright terms: Public domain