Axiom ax-13 804

Description: Axiom of Equality. One of the 3 non-logical predicate axioms of our predicate calculus. It substitutes equal variables into the left-hand side of the ∈ binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments.

Assertion

Ref	Expression
ax-13	⊢ (x = y → (x ∈ z → y ∈ z))

Detailed syntax breakdown of Axiom ax-13

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	wel 803	. . 3 wff x ∈ z
6	2, 4	wel 803	. . 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:  a13b 819

metamath.org