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	$$⊢\phi \to A\in B$$
	spcdvw.2	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	spcdvw	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spcdvw.1	$$⊢\phi \to A\in B$$
2		spcdvw.2	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
3	2	biimpd	$$⊢x=A\to \left(\psi \to \chi \right)$$
4	3	ax-gen	$$⊢\forall x\left(x=A\to \left(\psi \to \chi \right)\right)$$
5		nfv	$$⊢Ⅎx\chi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
7	5 6	spcimgfi1	$$⊢\forall x\left(x=A\to \left(\psi \to \chi \right)\right)\to \left(A\in B\to \left(\forall x\psi \to \chi \right)\right)$$
8	4 1 7	mpsyl	$$⊢\phi \to \left(\forall x\psi \to \chi \right)$$