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 -> ( th <-> ch ) )
	rspc2vd.b	|- ( y = B -> ( ch <-> ps ) )
	rspc2vd.c	|- ( ph -> A e. C )
	rspc2vd.d	|- ( ( ph /\ x = A ) -> D = E )
	rspc2vd.e	|- ( ph -> B e. E )
Assertion	rspc2vd	|- ( ph -> ( A. x e. C A. y e. D th -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rspc2vd.a	|- ( x = A -> ( th <-> ch ) )
2		rspc2vd.b	|- ( y = B -> ( ch <-> ps ) )
3		rspc2vd.c	|- ( ph -> A e. C )
4		rspc2vd.d	|- ( ( ph /\ x = A ) -> D = E )
5		rspc2vd.e	|- ( ph -> B e. E )
6	3 4	csbied	|- ( ph -> [_ A / x ]_ D = E )
7	5 6	eleqtrrd	|- ( ph -> B e. [_ A / x ]_ D )
8		nfcsb1v	|- F/_ x [_ A / x ]_ D
9		nfv	|- F/ x ch
10	8 9	nfralw	|- F/ x A. y e. [_ A / x ]_ D ch
11		csbeq1a	|- ( x = A -> D = [_ A / x ]_ D )
12	11 1	raleqbidv	|- ( x = A -> ( A. y e. D th <-> A. y e. [_ A / x ]_ D ch ) )
13	10 12	rspc	|- ( A e. C -> ( A. x e. C A. y e. D th -> A. y e. [_ A / x ]_ D ch ) )
14	3 13	syl	|- ( ph -> ( A. x e. C A. y e. D th -> A. y e. [_ A / x ]_ D ch ) )
15	2	rspcv	|- ( B e. [_ A / x ]_ D -> ( A. y e. [_ A / x ]_ D ch -> ps ) )
16	7 14 15	sylsyld	|- ( ph -> ( A. x e. C A. y e. D th -> ps ) )