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).
We prove in ax9 that this axiom can be recovered from its weakened version ax9v where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 should be ax9v . See the comment of ax9v for more details on these matters. (Contributed by NM, 21-Jun-1993) (Revised by BJ, 7-Dec-2020) Use ax9 instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-9 | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | 0 | cv | ⊢ 𝑥 |
| 2 | vy | ⊢ 𝑦 | |
| 3 | 2 | cv | ⊢ 𝑦 |
| 4 | 1 3 | wceq | ⊢ 𝑥 = 𝑦 |
| 5 | vz | ⊢ 𝑧 | |
| 6 | 5 | cv | ⊢ 𝑧 |
| 7 | 6 1 | wcel | ⊢ 𝑧 ∈ 𝑥 |
| 8 | 6 3 | wcel | ⊢ 𝑧 ∈ 𝑦 |
| 9 | 7 8 | wi | ⊢ ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) |
| 10 | 4 9 | wi | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) |