Theorem spcimgfi1OLD

Description: Obsolete version of spcimgfi1 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spcimgfi1.1	|- F/ x ps
	spcimgfi1.2	|- F/_ x A
Assertion	spcimgfi1OLD	|- ( 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		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	biimtrid	|- ( 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	imbitrdi	|- ( 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 ) ) )