Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv1v with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbv1.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| cbv1.2 | ⊢ Ⅎ 𝑦 𝜑 | ||
| cbv1.3 | ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 ) | ||
| cbv1.4 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | ||
| cbv1.5 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) | ||
| Assertion | cbv1 | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbv1.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | cbv1.2 | ⊢ Ⅎ 𝑦 𝜑 | |
| 3 | cbv1.3 | ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 ) | |
| 4 | cbv1.4 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | |
| 5 | cbv1.5 | ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) ) ) | |
| 6 | 2 3 | nfim1 | ⊢ Ⅎ 𝑦 ( 𝜑 → 𝜓 ) |
| 7 | 1 4 | nfim1 | ⊢ Ⅎ 𝑥 ( 𝜑 → 𝜒 ) |
| 8 | 5 | com12 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ( 𝜓 → 𝜒 ) ) ) |
| 9 | 8 | a2d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) ) |
| 10 | 6 7 9 | cbv3 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑦 ( 𝜑 → 𝜒 ) ) |
| 11 | 1 | 19.21 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 𝜓 ) ) |
| 12 | 2 | 19.21 | ⊢ ( ∀ 𝑦 ( 𝜑 → 𝜒 ) ↔ ( 𝜑 → ∀ 𝑦 𝜒 ) ) |
| 13 | 10 11 12 | 3imtr3i | ⊢ ( ( 𝜑 → ∀ 𝑥 𝜓 ) → ( 𝜑 → ∀ 𝑦 𝜒 ) ) |
| 14 | 13 | pm2.86i | ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) ) |