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