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