**Changing EXIST-ALL to ALL-EXIST**

**Version 2.0 (New)**
Theorem: EXIST(a):ALL(b):[P(b) => R(a,b)]
=> ALL(b):[P(b)=>EXIST(a):R(a,b)]
Proof:
Suppose...
1 EXIST(a):ALL(b):[P(b) => R(a,b)]
Premise
Suppose further...
2 P(y)
Premise
Apply initial premise for a=x and b=y
3 ALL(b):[P(b) => R(x,b)]
E Spec, 1
4 P(y) => R(x,y)
U Spec, 3
Apply Detachment Rule on lines 4 and 2
5 R(x,y)
Detach, 4, 2
x was introduced here by Existential Specification on
line 3. y was introduced by Premise on line 2.
By applying the the Conclusion Rule here, x and y are
automatically generalized by existential and universal
generalization respectively, and we introduce '=>'. The
user chooses only the names of bound variables.
6 ALL(b):[P(b) => EXIST(a):R(a,b)]
Conclusion, 2
Applying the Conclusion Rule once more...
As Required:
7 EXIST(a):ALL(b):[P(b) => R(a,b)]
=> ALL(b):[P(b) => EXIST(a):R(a,b)]
Conclusion, 1