Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmov with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 16-Jun-2017) (Revised by GG, 30-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvrmovw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | cbvrmovw | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvrmovw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | eleq1w | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) | |
| 3 | 2 1 | anbi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) |
| 4 | 3 | cbvmovw | ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) |
| 5 | df-rmo | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) | |
| 6 | df-rmo | ⊢ ( ∃* 𝑦 ∈ 𝐴 𝜓 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) | |
| 7 | 4 5 6 | 3bitr4i | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |