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