Theorem rspc2daf

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

	Ref	Expression
Hypotheses	sbc2iedf.1	⊢ Ⅎ 𝑥 𝜑
	sbc2iedf.2	⊢ Ⅎ 𝑦 𝜑
	sbc2iedf.3	⊢ Ⅎ 𝑥 𝜒
	sbc2iedf.4	⊢ Ⅎ 𝑦 𝜒
	sbc2iedf.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sbc2iedf.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	sbc2iedf.7	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
	rspc2daf.8	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜓 )
Assertion	rspc2daf	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		sbc2iedf.1	⊢ Ⅎ 𝑥 𝜑
2		sbc2iedf.2	⊢ Ⅎ 𝑦 𝜑
3		sbc2iedf.3	⊢ Ⅎ 𝑥 𝜒
4		sbc2iedf.4	⊢ Ⅎ 𝑦 𝜒
5		sbc2iedf.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		sbc2iedf.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
7		sbc2iedf.7	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
8		rspc2daf.8	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜓 )
9		nfcv	⊢ Ⅎ 𝑥 𝑊
10		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜓
11	9 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑊 [ 𝐴 / 𝑥 ] 𝜓
12		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝐴
13	2 12	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 )
14		sbceq1a	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )
16	13 15	ralbid	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ∀ 𝑦 ∈ 𝑊 𝜓 ↔ ∀ 𝑦 ∈ 𝑊 [ 𝐴 / 𝑥 ] 𝜓 ) )
17	1 11 5 16	rspcdf	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜓 → ∀ 𝑦 ∈ 𝑊 [ 𝐴 / 𝑥 ] 𝜓 ) )
18	8 17	mpd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑊 [ 𝐴 / 𝑥 ] 𝜓 )
19		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓
20		sbceq1a	⊢ ( 𝑦 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 ) )
22	2 19 6 21	rspcdf	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑊 [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 ) )
23	18 22	mpd	⊢ ( 𝜑 → [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 )
24	1 2 3 4 5 6 7	sbc2iedf	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
25		sbccom	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 )
26	24 25	bitr3di	⊢ ( 𝜑 → ( 𝜒 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜓 ) )
27	23 26	mpbird	⊢ ( 𝜑 → 𝜒 )