Axiom ax-8 798

Description: Axiom of Equality. One of the 5 equality axioms of predicate calculus. This is similar to, but not quite, a transitive law for equality (proved later as eqt 814). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105.

Axioms ax-8 798 through ax-16 922 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 922 and ax-17 925 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 922 and ax-17 925 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	. . 3 set x
2		vy	. . 3 set y
3	1, 2	weq 797	. 2 wff x = y
4		vz	. . . 4 set z
5	1, 4	weq 797	. . 3 wff x = z
6	2, 4	weq 797	. . 3 wff y = z
7	5, 6	wi 2	. 2 wff (x = z → y = z)
8	3, 7	wi 2	1 wff (x = y → (x = z → y = z))

This axiom is referenced by:  eqcom 811  eqt 814  a8b 817  eqvin.l1 851  del43 856  hbsb4 905  mo 1020  axextnd 3737

metamath.org