Metamath Proof Explorer

Theorem rspc8v

Description: 8-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025)

Ref Expression
Hypotheses rspc8v.1 ⊢x=A→φ↔χ
rspc8v.2 ⊢y=B→χ↔θ
rspc8v.3 ⊢z=C→θ↔τ
rspc8v.4 ⊢w=D→τ↔η
rspc8v.5 ⊢p=E→η↔ζ
rspc8v.6 ⊢q=F→ζ↔σ
rspc8v.7 ⊢r=G→σ↔ρ
rspc8v.8 ⊢s=H→ρ↔ψ
Assertion rspc8v ⊢A∈R∧B∈S∧C∈T∧D∈U∧E∈V∧F∈W∧G∈X∧H∈Y→∀x∈R∀y∈S∀z∈T∀w∈U∀p∈V∀q∈W∀r∈X∀s∈Yφ→ψ

Proof

Step Hyp Ref Expression
1 rspc8v.1 ⊢x=A→φ↔χ
2 rspc8v.2 ⊢y=B→χ↔θ
3 rspc8v.3 ⊢z=C→θ↔τ
4 rspc8v.4 ⊢w=D→τ↔η
5 rspc8v.5 ⊢p=E→η↔ζ
6 rspc8v.6 ⊢q=F→ζ↔σ
7 rspc8v.7 ⊢r=G→σ↔ρ
8 rspc8v.8 ⊢s=H→ρ↔ψ
9 1 4ralbidv ⊢x=A→∀p∈V∀q∈W∀r∈X∀s∈Yφ↔∀p∈V∀q∈W∀r∈X∀s∈Yχ
10 2 4ralbidv ⊢y=B→∀p∈V∀q∈W∀r∈X∀s∈Yχ↔∀p∈V∀q∈W∀r∈X∀s∈Yθ
11 3 4ralbidv ⊢z=C→∀p∈V∀q∈W∀r∈X∀s∈Yθ↔∀p∈V∀q∈W∀r∈X∀s∈Yτ
12 4 4ralbidv ⊢w=D→∀p∈V∀q∈W∀r∈X∀s∈Yτ↔∀p∈V∀q∈W∀r∈X∀s∈Yη
13 9 10 11 12 rspc4v ⊢A∈R∧B∈S∧C∈T∧D∈U→∀x∈R∀y∈S∀z∈T∀w∈U∀p∈V∀q∈W∀r∈X∀s∈Yφ→∀p∈V∀q∈W∀r∈X∀s∈Yη
14 5 6 7 8 rspc4v ⊢E∈V∧F∈W∧G∈X∧H∈Y→∀p∈V∀q∈W∀r∈X∀s∈Yη→ψ
15 13 14 sylan9 ⊢A∈R∧B∈S∧C∈T∧D∈U∧E∈V∧F∈W∧G∈X∧H∈Y→∀x∈R∀y∈S∀z∈T∀w∈U∀p∈V∀q∈W∀r∈X∀s∈Yφ→ψ