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

Metamath Proof Explorer

Theorem cbvral8vw

Description: Change bound variables of octuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025)

Ref Expression
Hypotheses cbvral8vw.1 ⊢ x = a → φ ↔ χ
cbvral8vw.2 ⊢ y = b → χ ↔ θ
cbvral8vw.3 ⊢ z = c → θ ↔ τ
cbvral8vw.4 ⊢ w = d → τ ↔ η
cbvral8vw.5 ⊢ p = e → η ↔ ζ
cbvral8vw.6 ⊢ q = f → ζ ↔ σ
cbvral8vw.7 ⊢ r = g → σ ↔ ρ
cbvral8vw.8 ⊢ s = h → ρ ↔ ψ
Assertion cbvral8vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ e ∈ E ∀ f ∈ F ∀ g ∈ G ∀ h ∈ H ψ

Proof

Step Hyp Ref Expression
1 cbvral8vw.1 ⊢ x = a → φ ↔ χ
2 cbvral8vw.2 ⊢ y = b → χ ↔ θ
3 cbvral8vw.3 ⊢ z = c → θ ↔ τ
4 cbvral8vw.4 ⊢ w = d → τ ↔ η
5 cbvral8vw.5 ⊢ p = e → η ↔ ζ
6 cbvral8vw.6 ⊢ q = f → ζ ↔ σ
7 cbvral8vw.7 ⊢ r = g → σ ↔ ρ
8 cbvral8vw.8 ⊢ s = h → ρ ↔ ψ
9 1 4ralbidv ⊢ x = a → ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H φ ↔ ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H χ
10 2 4ralbidv ⊢ y = b → ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H χ ↔ ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H θ
11 3 4ralbidv ⊢ z = c → ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H θ ↔ ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H τ
12 4 4ralbidv ⊢ w = d → ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H τ ↔ ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H η
13 9 10 11 12 cbvral4vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H η
14 5 6 7 8 cbvral4vw ⊢ ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H η ↔ ∀ e ∈ E ∀ f ∈ F ∀ g ∈ G ∀ h ∈ H ψ
15 14 4ralbii ⊢ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H η ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ e ∈ E ∀ f ∈ F ∀ g ∈ G ∀ h ∈ H ψ
16 13 15 bitri ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F ∀ r ∈ G ∀ s ∈ H φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ e ∈ E ∀ f ∈ F ∀ g ∈ G ∀ h ∈ H ψ