This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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