Description: Variation on nfald which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016) Usage of this theorem is discouraged because it depends on ax-13 . Use nfald instead. (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 | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |