Theorem rspc2dv

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025)

	Ref	Expression
Hypotheses	rspc2dv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
	rspc2dv.2	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜒 ) )
	rspc2dv.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜓 )
	rspc2dv.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	rspc2dv.5	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
Assertion	rspc2dv	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		rspc2dv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
2		rspc2dv.2	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜒 ) )
3		rspc2dv.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜓 )
4		rspc2dv.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
5		rspc2dv.5	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
6	1 2	rspc2va	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜓 ) → 𝜒 )
7	4 5 3 6	syl21anc	⊢ ( 𝜑 → 𝜒 )