Theorem cbvral6vw 3250

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

Hypotheses

Ref	Expression
cbvral6vw.1	⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
cbvral6vw.2	⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
cbvral6vw.3	⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
cbvral6vw.4	⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))
cbvral6vw.5	⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))
cbvral6vw.6	⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓))

Assertion

Ref	Expression
cbvral6vw	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓)

Distinct variable groups:   𝐴,𝑎,𝑥   𝜂,𝑤   𝜃,𝑦   𝜓,𝑞   𝜃,𝑐   𝜏,𝑑   𝜁,𝑝   𝜒,𝑥   𝜂,𝑒   𝜒,𝑏   𝜑,𝑎   𝜁,𝑓   𝐸,𝑐   𝑒,𝐸   𝐸,𝑑   𝐸,𝑏,𝑧   𝐷,𝑐   𝐷,𝑎,𝑥   𝐷,𝑏,𝑦,𝑧   𝐵,𝑎,𝑥   𝐵,𝑏,𝑦   𝐶,𝑎,𝑥   𝑒,𝐹,𝑝,𝑞   𝐹,𝑎,𝑥,𝑧,𝑞   𝐹,𝑏,𝑤,𝑦,𝑝,𝑞   𝐹,𝑐,𝑝,𝑞,𝑤,𝑧   𝐹,𝑑,𝑝,𝑞   𝜏,𝑧   𝐶,𝑐   𝐸,𝑎,𝑝,𝑤,𝑥,𝑦   𝑓,𝐹,𝑞   𝐶,𝑏,𝑦,𝑧   𝐷,𝑑,𝑤

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑏, 𝑐, 𝑑)   𝜓(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝜒(𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑎, 𝑐, 𝑑)   𝜃(𝑥, 𝑧, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑎, 𝑏, 𝑑)   𝜏(𝑥, 𝑦, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐)   𝜂(𝑥, 𝑦, 𝑧, 𝑓, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝜁(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑞, 𝑎, 𝑏, 𝑐, 𝑑)   𝐴(𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑏, 𝑐, 𝑑)   𝐵(𝑧, 𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑐, 𝑑)   𝐶(𝑤, 𝑒, 𝑓, 𝑞, 𝑝, 𝑑)   𝐷(𝑒, 𝑓, 𝑞, 𝑝)   𝐸(𝑓, 𝑞)

Proof of Theorem cbvral6vw

Step	Hyp	Ref	Expression
1		cbvral6vw.1	. . . 4 ⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
2	1	2ralbidv 3228	. . 3 ⊢ (𝑥 = 𝑎 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒))
3		cbvral6vw.2	. . . 4 ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
4	3	2ralbidv 3228	. . 3 ⊢ (𝑦 = 𝑏 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜃))
5		cbvral6vw.3	. . . 4 ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
6	5	2ralbidv 3228	. . 3 ⊢ (𝑧 = 𝑐 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜃 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜏))
7		cbvral6vw.4	. . . 4 ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))
8	7	2ralbidv 3228	. . 3 ⊢ (𝑤 = 𝑑 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜏 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂))
9	2, 4, 6, 8	cbvral4vw 3249	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂)
10		cbvral6vw.5	. . . 4 ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))
11		cbvral6vw.6	. . . 4 ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓))
12	10, 11	cbvral2vw 3246	. . 3 ⊢ (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂 ↔ ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓)
13	12	4ralbii 3142	. 2 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓)
14	9, 13	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:  mulsproplemcbv  28319  mulsprop  28334