Natural deduction and predicate logic.

Hi ,

Can somebody tell me if line 10 is correct ? Did I do a mistake?


∀x(A ∨ B) ⊢ ∀x A∨B , Note: x is not free in B .

1.∀x(A∨B) premise

2.¬(∀A∨B) assumption

3.x0

4.(A∨B) [x/x0] (∀xe),1

5.A[x/x0] ∨ B x is not free in B

6.B Assumption

7.∀x A ∨ B (Vi),6

8.⊥ (¬e) 2,7

9.A[x/x0] (⊥e),8

10.∀xA (∀x)i,3-9

11.∀A∨B (vi),10

12.⊥ (¬e) 2 , 11

13.¬¬(∀A∨B) (¬i),2-12

14.∀A∨B (¬¬e) ,13