Theorem rspc2daf

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

	Ref	Expression
Hypotheses	sbc2iedf.1	$$⊢Ⅎx\phi$$
	sbc2iedf.2	$$⊢Ⅎy\phi$$
	sbc2iedf.3	$$⊢Ⅎx\chi$$
	sbc2iedf.4	$$⊢Ⅎy\chi$$
	sbc2iedf.5	$$⊢\phi \to A\in V$$
	sbc2iedf.6	$$⊢\phi \to B\in W$$
	sbc2iedf.7	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
	rspc2daf.8	$$⊢\phi \to \forall x\in V\forall y\in W\psi$$
Assertion	rspc2daf	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		sbc2iedf.1	$$⊢Ⅎx\phi$$
2		sbc2iedf.2	$$⊢Ⅎy\phi$$
3		sbc2iedf.3	$$⊢Ⅎx\chi$$
4		sbc2iedf.4	$$⊢Ⅎy\chi$$
5		sbc2iedf.5	$$⊢\phi \to A\in V$$
6		sbc2iedf.6	$$⊢\phi \to B\in W$$
7		sbc2iedf.7	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
8		rspc2daf.8	$$⊢\phi \to \forall x\in V\forall y\in W\psi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xW$$
10		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
11	9 10	nfralw	$$⊢Ⅎx\forall y\in W\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
12		nfv	$$⊢Ⅎyx=A$$
13	2 12	nfan	$$⊢Ⅎy\left(\phi \wedge x=A\right)$$
14		sbceq1a	$$⊢x=A\to \left(\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
15	14	adantl	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
16	13 15	ralbid	$$⊢\left(\phi \wedge x=A\right)\to \left(\forall y\in W\psi \leftrightarrow \forall y\in W\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
17	1 11 5 16	rspcdf	$$⊢\phi \to \left(\forall x\in V\forall y\in W\psi \to \forall y\in W\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
18	8 17	mpd	$$⊢\phi \to \forall y\in W\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
19		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
20		sbceq1a	$$⊢y=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
21	20	adantl	$$⊢\left(\phi \wedge y=B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
22	2 19 6 21	rspcdf	$$⊢\phi \to \left(\forall y\in W\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
23	18 22	mpd	$$⊢\phi \to \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
24	1 2 3 4 5 6 7	sbc2iedf	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
25		sbccom	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$
26	24 25	bitr3di	$$⊢\phi \to \left(\chi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
27	23 26	mpbird	$$⊢\phi \to \chi$$