Axiom ax-9 2116

Description: Axiom of Right Equality for Binary Predicate. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of an arbitrary binary predicate ∈, which we will use for the set membership relation when set theory is introduced. This axiom scheme is a sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose general form cannot be represented with our notation. Also appears as Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint).

We prove in ax9 2120 that this axiom can be recovered from its weakened version ax9v 2117 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 2116 should be ax9v 2117. See the comment of ax9v 2117 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 2120 instead. (New usage is discouraged.)

Assertion

Ref	Expression
ax-9	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))

Detailed syntax breakdown of Axiom ax-9

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		vy	. . 3 setvar 𝑦
3	1, 2	weq 1966	. 2 wff 𝑥 = 𝑦
4		vz	. . . 4 setvar 𝑧
5	4, 1	wel 2107	. . 3 wff 𝑧 ∈ 𝑥
6	4, 2	wel 2107	. . 3 wff 𝑧 ∈ 𝑦
7	5, 6	wi 4	. 2 wff (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)
8	3, 7	wi 4	1 wff (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))

This axiom is referenced by:  ax9v  2117