Theorem spcgft

Description: A closed version of spcgf . (Contributed by Andrew Salmon, 6-Jun-2011) (Revised by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	spcimgfi1.1	|- F/ x ps
	spcimgfi1.2	|- F/_ x A
Assertion	spcgft	|- ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		spcimgfi1.1	|- F/ x ps
2		spcimgfi1.2	|- F/_ x A
3		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
4	3	imim2i	|- ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph -> ps ) ) )
5	4	alimi	|- ( A. x ( x = A -> ( ph <-> ps ) ) -> A. x ( x = A -> ( ph -> ps ) ) )
6	1 2	spcimgfi1	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )
7	5 6	syl	|- ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )