Theorem spcdvw

Description: A version of spcdv where ps and ch are direct substitutions of each other. This theorem is useful because it does not require ph and x to be distinct variables. (Contributed by Emmett Weisz, 12-Apr-2020)

	Ref	Expression
Hypotheses	spcdvw.1	|- ( ph -> A e. B )
	spcdvw.2	|- ( x = A -> ( ps <-> ch ) )
Assertion	spcdvw	|- ( ph -> ( A. x ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		spcdvw.1	|- ( ph -> A e. B )
2		spcdvw.2	|- ( x = A -> ( ps <-> ch ) )
3	2	biimpd	|- ( x = A -> ( ps -> ch ) )
4	3	ax-gen	|- A. x ( x = A -> ( ps -> ch ) )
5		nfv	|- F/ x ch
6		nfcv	|- F/_ x A
7	5 6	spcimgft	|- ( A. x ( x = A -> ( ps -> ch ) ) -> ( A e. B -> ( A. x ps -> ch ) ) )
8	4 1 7	mpsyl	|- ( ph -> ( A. x ps -> ch ) )