Description: Rule used to change bound variables, using implicit substitution. Version of cbv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Gino Giotto, 10-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbv2w.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| cbv2w.2 | ⊢ Ⅎ 𝑦 𝜑 | ||
| cbv2w.3 | ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 ) | ||
| cbv2w.4 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | ||
| cbv2w.5 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) ) | ||
| Assertion | cbv2w | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbv2w.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | cbv2w.2 | ⊢ Ⅎ 𝑦 𝜑 | |
| 3 | cbv2w.3 | ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 ) | |
| 4 | cbv2w.4 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | |
| 5 | cbv2w.5 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) ) | |
| 6 | biimp | ⊢ ( ( 𝜓 ↔ 𝜒 ) → ( 𝜓 → 𝜒 ) ) | |
| 7 | 5 6 | syl6 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) |
| 8 | 1 2 3 4 7 | cbv1v | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) ) |
| 9 | equcomi | ⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 ) | |
| 10 | biimpr | ⊢ ( ( 𝜓 ↔ 𝜒 ) → ( 𝜒 → 𝜓 ) ) | |
| 11 | 9 5 10 | syl56 | ⊢ ( 𝜑 → ( 𝑦 = 𝑥 → ( 𝜒 → 𝜓 ) ) ) |
| 12 | 2 1 4 3 11 | cbv1v | ⊢ ( 𝜑 → ( ∀ 𝑦 𝜒 → ∀ 𝑥 𝜓 ) ) |
| 13 | 8 12 | impbid | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) ) |