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

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 φ → ψ