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

Metamath Proof Explorer

Theorem cbvral6vw

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

Ref Expression
Hypotheses cbvral6vw.1 ⊢ x = a → φ ↔ χ
cbvral6vw.2 ⊢ y = b → χ ↔ θ
cbvral6vw.3 ⊢ z = c → θ ↔ τ
cbvral6vw.4 ⊢ w = d → τ ↔ η
cbvral6vw.5 ⊢ p = e → η ↔ ζ
cbvral6vw.6 ⊢ q = f → ζ ↔ ψ
Assertion cbvral6vw ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F φ ↔ ∀ a ∈ A ∀ b ∈ B ∀ c ∈ C ∀ d ∈ D ∀ e ∈ E ∀ f ∈ F ψ

Proof

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