Theorem cbvral4vw 3249

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

Hypotheses

Ref	Expression
cbvral4vw.1	⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
cbvral4vw.2	⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
cbvral4vw.3	⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
cbvral4vw.4	⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜓))

Assertion

Ref	Expression
cbvral4vw	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 𝜓)

Distinct variable groups:   𝑥,𝑎,𝐴   𝑦,𝑎,𝐵,𝑥   𝑦,𝑏,𝐵   𝐶,𝑎,𝑥   𝐶,𝑏,𝑦   𝑧,𝑐,𝐶   𝑧,𝑎,𝑤,𝐷,𝑥,𝑦   𝑧,𝑏,𝑤,𝐷   𝑤,𝑐,𝐷   𝑤,𝑑,𝐷   𝜑,𝑎   𝜒,𝑏   𝜃,𝑐   𝜒,𝑥   𝜏,𝑑   𝜓,𝑤   𝜏,𝑧   𝜃,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑏, 𝑐, 𝑑)   𝜓(𝑥, 𝑦, 𝑧, 𝑎, 𝑏, 𝑐, 𝑑)   𝜒(𝑦, 𝑧, 𝑤, 𝑎, 𝑐, 𝑑)   𝜃(𝑥, 𝑧, 𝑤, 𝑎, 𝑏, 𝑑)   𝜏(𝑥, 𝑦, 𝑤, 𝑎, 𝑏, 𝑐)   𝐴(𝑦, 𝑧, 𝑤, 𝑏, 𝑐, 𝑑)   𝐵(𝑧, 𝑤, 𝑐, 𝑑)   𝐶(𝑤, 𝑑)

Proof of Theorem cbvral4vw

Step	Hyp	Ref	Expression
1		cbvral4vw.1	. . . 4 ⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
2	1	ralbidv 3187	. . 3 ⊢ (𝑥 = 𝑎 → (∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑤 ∈ 𝐷 𝜒))
3		cbvral4vw.2	. . . 4 ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
4	3	ralbidv 3187	. . 3 ⊢ (𝑦 = 𝑏 → (∀𝑤 ∈ 𝐷 𝜒 ↔ ∀𝑤 ∈ 𝐷 𝜃))
5		cbvral4vw.3	. . . 4 ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
6	5	ralbidv 3187	. . 3 ⊢ (𝑧 = 𝑐 → (∀𝑤 ∈ 𝐷 𝜃 ↔ ∀𝑤 ∈ 𝐷 𝜏))
7	2, 4, 6	cbvral3vw 3248	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜏)
8		cbvral4vw.4	. . . 4 ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜓))
9	8	cbvralvw 3242	. . 3 ⊢ (∀𝑤 ∈ 𝐷 𝜏 ↔ ∀𝑑 ∈ 𝐷 𝜓)
10	9	3ralbii 3141	. 2 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜏 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 𝜓)
11	7, 10	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837  df-ral 3079

This theorem is used by:  cbvral6vw  3250  cbvral8vw  3251