Theorem rspc2vd

Description: Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class D for the second set variable y may depend on the first set variable x . (Contributed by AV, 29-Mar-2021)

	Ref	Expression
Hypotheses	rspc2vd.a	$$⊢x=A\to \left(\theta \leftrightarrow \chi \right)$$
	rspc2vd.b	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
	rspc2vd.c	$$⊢\phi \to A\in C$$
	rspc2vd.d	$$⊢\left(\phi \wedge x=A\right)\to D=E$$
	rspc2vd.e	$$⊢\phi \to B\in E$$
Assertion	rspc2vd	$$⊢\phi \to \left(\forall x\in C\forall y\in D\theta \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rspc2vd.a	$$⊢x=A\to \left(\theta \leftrightarrow \chi \right)$$
2		rspc2vd.b	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
3		rspc2vd.c	$$⊢\phi \to A\in C$$
4		rspc2vd.d	$$⊢\left(\phi \wedge x=A\right)\to D=E$$
5		rspc2vd.e	$$⊢\phi \to B\in E$$
6	3 4	csbied	$$⊢\phi \to ⦋A/x⦌D=E$$
7	5 6	eleqtrrd	$$⊢\phi \to B\in ⦋A/x⦌D$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌D$$
9		nfv	$$⊢Ⅎx\chi$$
10	8 9	nfralw	$$⊢Ⅎx\forall y\in ⦋A/x⦌D\chi$$
11		csbeq1a	$$⊢x=A\to D=⦋A/x⦌D$$
12	11 1	raleqbidv	$$⊢x=A\to \left(\forall y\in D\theta \leftrightarrow \forall y\in ⦋A/x⦌D\chi \right)$$
13	10 12	rspc	$$⊢A\in C\to \left(\forall x\in C\forall y\in D\theta \to \forall y\in ⦋A/x⦌D\chi \right)$$
14	3 13	syl	$$⊢\phi \to \left(\forall x\in C\forall y\in D\theta \to \forall y\in ⦋A/x⦌D\chi \right)$$
15	2	rspcv	$$⊢B\in ⦋A/x⦌D\to \left(\forall y\in ⦋A/x⦌D\chi \to \psi \right)$$
16	7 14 15	sylsyld	$$⊢\phi \to \left(\forall x\in C\forall y\in D\theta \to \psi \right)$$