This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝜒 )