Metamath Proof Explorer

Theorem bj-spimvwt

Description: Closed form of spimvw . See also spimt . (Contributed by BJ, 8-Nov-2021)

Ref Expression
Assertion bj-spimvwt 
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ph -> ps ) )

Proof

Step Hyp Ref Expression
1 alequexv 
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> E. x ( ph -> ps ) )
2 19.36v 
 |-  ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
3 1 2 sylib 
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ph -> ps ) )