Theorem bj-dvelimdv1

Description: Curried (exported) form of bj-dvelimdv (of course, one is directly provable from the other, but we keep this proof for illustration purposes). (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-dvelimdv.nf	|- ( ph -> F/ x ch )
	bj-dvelimdv.is	|- ( z = y -> ( ch <-> ps ) )
Assertion	bj-dvelimdv1	|- ( ph -> ( -. A. x x = y -> F/ x ps ) )

Proof

Step	Hyp	Ref	Expression
1		bj-dvelimdv.nf	|- ( ph -> F/ x ch )
2		bj-dvelimdv.is	|- ( z = y -> ( ch <-> ps ) )
3		nfeqf2	|- ( -. A. x x = y -> F/ x z = y )
4		bj-nfimt	|- ( F/ x z = y -> ( F/ x ch -> F/ x ( z = y -> ch ) ) )
5	3 1 4	syl2imc	|- ( ph -> ( -. A. x x = y -> F/ x ( z = y -> ch ) ) )
6	5	alrimdv	|- ( ph -> ( -. A. x x = y -> A. z F/ x ( z = y -> ch ) ) )
7		bj-nfalt	|- ( A. z F/ x ( z = y -> ch ) -> F/ x A. z ( z = y -> ch ) )
8	2	equsalvw	|- ( A. z ( z = y -> ch ) <-> ps )
9	8	nfbii	|- ( F/ x A. z ( z = y -> ch ) <-> F/ x ps )
10	6 7 9	bj-syl66ib	|- ( ph -> ( -. A. x x = y -> F/ x ps ) )