Theorem spcimgfi1

Description: A closed version of spcimgf . (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by Wolf Lammen, 27-Jul-2025)

	Ref	Expression
Hypotheses	spcimgfi1.1	|- F/ x ps
	spcimgfi1.2	|- F/_ x A
Assertion	spcimgfi1	|- ( 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		spcimgft	|- ( ( ( F/_ x A /\ F/ x ps ) /\ A. x ( x = A -> ( ph -> ps ) ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )
4	3	ex	|- ( ( F/_ x A /\ F/ x ps ) -> ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) ) )
5	2 1 4	mp2an	|- ( A. x ( x = A -> ( ph -> ps ) ) -> ( A e. B -> ( A. x ph -> ps ) ) )