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