Metamath Proof Explorer

Theorem spcimgft

Description: Closed theorem form of spcimgf . (Contributed by Wolf Lammen, 28-Jul-2025)

Ref Expression
Assertion spcimgft 
|- ( ( ( F/_ x A /\ F/ x ps ) /\ A. x ( x = A -> ( ph -> ps ) ) ) -> ( A e. V -> ( A. x ph -> ps ) ) )

Proof

Step Hyp Ref Expression
1 elissetv 
 |-  ( A e. V -> E. y y = A )
2 cbvexeqsetf 
 |-  ( F/_ x A -> ( E. x x = A <-> E. y y = A ) )
3 1 2 imbitrrid 
 |-  ( F/_ x A -> ( A e. V -> E. x x = A ) )
4 pm2.04 
 |-  ( ( x = A -> ( ph -> ps ) ) -> ( ph -> ( x = A -> ps ) ) )
5 4 al2imi 
 |-  ( A. x ( x = A -> ( ph -> ps ) ) -> ( A. x ph -> A. x ( x = A -> ps ) ) )
6 19.23t 
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
7 6 biimpd 
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) -> ( E. x x = A -> ps ) ) )
8 5 7 sylan9r 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph -> ps ) ) ) -> ( A. x ph -> ( E. x x = A -> ps ) ) )
9 8 com23 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph -> ps ) ) ) -> ( E. x x = A -> ( A. x ph -> ps ) ) )
10 3 9 sylan9 
 |-  ( ( F/_ x A /\ ( F/ x ps /\ A. x ( x = A -> ( ph -> ps ) ) ) ) -> ( A e. V -> ( A. x ph -> ps ) ) )
11 10 anassrs 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ A. x ( x = A -> ( ph -> ps ) ) ) -> ( A e. V -> ( A. x ph -> ps ) ) )