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

Metamath Proof Explorer

Theorem cbvral4vw

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

Ref Expression
Hypotheses cbvral4vw.1 ⊢ x = a → φ ↔ χ
cbvral4vw.2 ⊢ y = b → χ ↔ θ
cbvral4vw.3 ⊢ z = c → θ ↔ τ
cbvral4vw.4 ⊢ w = d → τ ↔ ψ
Assertion cbvral4vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ψ

Proof

Step Hyp Ref Expression
1 cbvral4vw.1 ⊢ x = a → φ ↔ χ
2 cbvral4vw.2 ⊢ y = b → χ ↔ θ
3 cbvral4vw.3 ⊢ z = c → θ ↔ τ
4 cbvral4vw.4 ⊢ w = d → τ ↔ ψ
5 1 ralbidv ⊢ x = a → ∀ w ∈ D φ ↔ ∀ w ∈ D χ
6 2 ralbidv ⊢ y = b → ∀ w ∈ D χ ↔ ∀ w ∈ D θ
7 3 ralbidv ⊢ z = c → ∀ w ∈ D θ ↔ ∀ w ∈ D τ
8 5 6 7 cbvral3vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ w ∈ D τ
9 4 cbvralvw ⊢ ∀ w ∈ D τ ↔ ∀ d ∈ D ψ
10 9 3ralbii ⊢ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ w ∈ D τ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ψ
11 8 10 bitri ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ψ