Metamath Proof Explorer


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 ) ) )