Axiom ax-14 1714

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 e., 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). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ax-14	|- (x = y -> (z e. x -> z e. y))

Detailed syntax breakdown of Axiom ax-14

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		vy	. . 3 setvar y
3	1, 2	weq 1643	. 2 wff x = y
4		vz	. . . 4 setvar z
5	4, 1	wel 1711	. . 3 wff z e. x
6	4, 2	wel 1711	. . 3 wff z e. y
7	5, 6	wi 4	. 2 wff (z e. x -> z e. y)
8	3, 7	wi 4	1 wff (x = y -> (z e. x -> z e. y))

This axiom is referenced by:  elequ2  1715  fv3  5342