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