Description: Variation on nfald which adds the hypothesis that x and y are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfald for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfald2.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| nfald2.2 | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) | ||
| Assertion | nfald2 | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfald2.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| 2 | nfald2.2 | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) | |
| 3 | nfnae | ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 | |
| 4 | 1 3 | nfan | ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) |
| 5 | 4 2 | nfald | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |
| 6 | 5 | ex | ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) ) |
| 7 | nfa1 | ⊢ Ⅎ 𝑦 ∀ 𝑦 𝜓 | |
| 8 | biidd | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜓 ↔ ∀ 𝑦 𝜓 ) ) | |
| 9 | 8 | drnf1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 ∀ 𝑦 𝜓 ↔ Ⅎ 𝑦 ∀ 𝑦 𝜓 ) ) |
| 10 | 7 9 | mpbiri | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |
| 11 | 6 10 | pm2.61d2 | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |