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