Theorem rspc2daf

Description: Double restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 4-Jul-2023)

	Ref	Expression
Hypotheses	sbc2iedf.1	|- F/ x ph
	sbc2iedf.2	|- F/ y ph
	sbc2iedf.3	|- F/ x ch
	sbc2iedf.4	|- F/ y ch
	sbc2iedf.5	|- ( ph -> A e. V )
	sbc2iedf.6	|- ( ph -> B e. W )
	sbc2iedf.7	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
	rspc2daf.8	|- ( ph -> A. x e. V A. y e. W ps )
Assertion	rspc2daf	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		sbc2iedf.1	|- F/ x ph
2		sbc2iedf.2	|- F/ y ph
3		sbc2iedf.3	|- F/ x ch
4		sbc2iedf.4	|- F/ y ch
5		sbc2iedf.5	|- ( ph -> A e. V )
6		sbc2iedf.6	|- ( ph -> B e. W )
7		sbc2iedf.7	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
8		rspc2daf.8	|- ( ph -> A. x e. V A. y e. W ps )
9		nfcv	|- F/_ x W
10		nfsbc1v	|- F/ x [. A / x ]. ps
11	9 10	nfralw	|- F/ x A. y e. W [. A / x ]. ps
12		nfv	|- F/ y x = A
13	2 12	nfan	|- F/ y ( ph /\ x = A )
14		sbceq1a	|- ( x = A -> ( ps <-> [. A / x ]. ps ) )
15	14	adantl	|- ( ( ph /\ x = A ) -> ( ps <-> [. A / x ]. ps ) )
16	13 15	ralbid	|- ( ( ph /\ x = A ) -> ( A. y e. W ps <-> A. y e. W [. A / x ]. ps ) )
17	1 11 5 16	rspcdf	|- ( ph -> ( A. x e. V A. y e. W ps -> A. y e. W [. A / x ]. ps ) )
18	8 17	mpd	|- ( ph -> A. y e. W [. A / x ]. ps )
19		nfsbc1v	|- F/ y [. B / y ]. [. A / x ]. ps
20		sbceq1a	|- ( y = B -> ( [. A / x ]. ps <-> [. B / y ]. [. A / x ]. ps ) )
21	20	adantl	|- ( ( ph /\ y = B ) -> ( [. A / x ]. ps <-> [. B / y ]. [. A / x ]. ps ) )
22	2 19 6 21	rspcdf	|- ( ph -> ( A. y e. W [. A / x ]. ps -> [. B / y ]. [. A / x ]. ps ) )
23	18 22	mpd	|- ( ph -> [. B / y ]. [. A / x ]. ps )
24	1 2 3 4 5 6 7	sbc2iedf	|- ( ph -> ( [. A / x ]. [. B / y ]. ps <-> ch ) )
25		sbccom	|- ( [. A / x ]. [. B / y ]. ps <-> [. B / y ]. [. A / x ]. ps )
26	24 25	bitr3di	|- ( ph -> ( ch <-> [. B / y ]. [. A / x ]. ps ) )
27	23 26	mpbird	|- ( ph -> ch )