Description: Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvraldva2.1 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| cbvraldva2.2 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) | ||
| Assertion | cbvraldva2 | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ∈ 𝐵 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvraldva2.1 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 2 | cbvraldva2.2 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐵 ) | |
| 3 | simpr | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 ) | |
| 4 | 3 2 | eleq12d | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) ) |
| 5 | 4 1 | imbi12d | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
| 6 | 5 | cbvaldvaw | ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) ) |
| 7 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) ) | |
| 8 | df-ral | ⊢ ( ∀ 𝑦 ∈ 𝐵 𝜒 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜒 ) ) | |
| 9 | 6 7 8 | 3bitr4g | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ∈ 𝐵 𝜒 ) ) |