Question regarding when substitutions can be made in FOL  (sci.logic)

Prove:  EyAx[P(y) -> P(x)] -> EyAx[P(y) -> (P(x) v Q(x)) ] (-from schema F -> F v G)

	1	EXIST(y):ALL(x):[P(y) => P(x)]
		Premise

	2	ALL(x):[P(b) => P(x)]
		E Spec, 1

	3	P(b) => P(a)
		U Spec, 2

		4	P(b)
			Premise

		5	P(a)
			Detach, 3, 4

		6	P(a) | Q(a)
			Arb Or, 5

	7	P(b) => P(a) | Q(a)
		Conclusion, 4

	8	ALL(x):[P(b) => P(x) | Q(x)]
		U Gen, 7

	9	EXIST(y):ALL(x):[P(y) => P(x) | Q(x)]
		E Gen, 8

10	EXIST(y):ALL(x):[P(y) => P(x)]
	=> EXIST(y):ALL(x):[P(y) => P(x) | Q(x)]
	Conclusion, 1