Metamath Proof Explorer


Theorem bj-spimtv

Description: Version of spimt with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 14-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-spimtv
|- ( ( F/ x ps /\ A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. x ph -> ps ) )

Proof

Step Hyp Ref Expression
1 ax6ev
 |-  E. x x = y
2 exim
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> ( E. x x = y -> E. x ( ph -> ps ) ) )
3 1 2 mpi
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> E. x ( ph -> ps ) )
4 19.35
 |-  ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
5 3 4 sylib
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ph -> E. x ps ) )
6 19.9t
 |-  ( F/ x ps -> ( E. x ps <-> ps ) )
7 6 biimpd
 |-  ( F/ x ps -> ( E. x ps -> ps ) )
8 5 7 sylan9r
 |-  ( ( F/ x ps /\ A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. x ph -> ps ) )