Theorem spcimgft

Description: A closed version of spcimgf . (Contributed by Mario Carneiro, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		spcimgft.1	|- F/ x ps
2		spcimgft.2	|- F/_ x A
3		elex	|- ( A e. B -> A e. _V )
4	2	issetf	|- ( A e. _V <-> E. x x = A )
5		exim	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( E. x x = A -> E. x ( ph -> ps ) ) )
6	4 5	syl5bi	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. _V -> E. x ( ph -> ps ) ) )
7	1	19.36	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
8	6 7	syl6ib	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. _V -> ( A. x ph -> ps ) ) )
9	3 8	syl5	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )