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