Theorem cbvral8vw 3249

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

Hypotheses

Ref	Expression
cbvral8vw.1	⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
cbvral8vw.2	⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
cbvral8vw.3	⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
cbvral8vw.4	⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))
cbvral8vw.5	⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))
cbvral8vw.6	⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜎))
cbvral8vw.7	⊢ (𝑟 = 𝑔 → (𝜎 ↔ 𝜌))
cbvral8vw.8	⊢ (𝑠 = ℎ → (𝜌 ↔ 𝜓))

Assertion

Ref	Expression
cbvral8vw	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓)

Distinct variable groups:   𝐴,𝑎,𝑥   𝐹,𝑎,𝑞,𝑤,𝑥,𝑦,𝑧   𝜁,𝑓   𝜌,𝑟   𝜌,ℎ   𝑔,𝐺,𝑟   𝜎,𝑞   𝐺,𝑑   𝜂,𝑤   𝜂,𝑒   𝜃,𝑦   𝐻,𝑐,𝑠   ℎ,𝐻,𝑠   𝑒,𝐺   𝜏,𝑧   𝜓,𝑠   𝜏,𝑑   𝐺,𝑐,𝑟   𝐹,𝑐,𝑞   𝜃,𝑐   𝐹,𝑑   𝐹,𝑏   𝐺,𝑏,𝑤,𝑧   𝑒,𝐹,𝑝   𝜑,𝑎   𝑓,𝐺   𝑓,𝐹   𝜁,𝑝   𝜒,𝑏   𝐵,𝑏   𝐶,𝑐   𝐶,𝑏   𝐸,𝑎,𝑥   𝐸,𝑐,𝑝   𝐸,𝑏,𝑦,𝑧   𝑒,𝐸   𝐻,𝑏,𝑝,𝑞,𝑟,𝑧,𝑠   𝜎,𝑔   𝐻,𝑑,𝑞,𝑟,𝑠   𝐺,𝑎,𝑝,𝑞,𝑥,𝑦   𝐵,𝑎,𝑥,𝑦   𝐶,𝑎,𝑥,𝑦,𝑧   𝐷,𝑎,𝑥   𝐷,𝑏,𝑦   𝑓,𝐻,𝑞,𝑟,𝑠   𝐸,𝑑,𝑤,𝑝   𝐷,𝑐,𝑤,𝑧   𝐻,𝑎,𝑤,𝑥,𝑦,𝑟,𝑠   𝐷,𝑑   𝑒,𝐻,𝑞,𝑟,𝑠   𝑔,𝐻,𝑠   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑏, 𝑐, 𝑑)   𝜓(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑟, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝜒(𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑎, 𝑐, 𝑑)   𝜃(𝑥, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑎, 𝑏, 𝑑)   𝜏(𝑥, 𝑦, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐)   𝜂(𝑥, 𝑦, 𝑧, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝜁(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑎, 𝑏, 𝑐, 𝑑)   𝜎(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, ℎ, 𝑠, 𝑟, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝜌(𝑥, 𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, 𝑠, 𝑞, 𝑝, 𝑎, 𝑏, 𝑐, 𝑑)   𝐴(𝑦, 𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑏, 𝑐, 𝑑)   𝐵(𝑧, 𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑐, 𝑑)   𝐶(𝑤, 𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝, 𝑑)   𝐷(𝑒, 𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞, 𝑝)   𝐸(𝑓, 𝑔, ℎ, 𝑠, 𝑟, 𝑞)   𝐹(𝑔, ℎ, 𝑠, 𝑟)   𝐺(ℎ, 𝑠)

Proof of Theorem cbvral8vw

Step	Hyp	Ref	Expression
1		cbvral8vw.1	. . . 4 ⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒))
2	1	4ralbidv 3230	. . 3 ⊢ (𝑥 = 𝑎 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜒))
3		cbvral8vw.2	. . . 4 ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃))
4	3	4ralbidv 3230	. . 3 ⊢ (𝑦 = 𝑏 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜒 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜃))
5		cbvral8vw.3	. . . 4 ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏))
6	5	4ralbidv 3230	. . 3 ⊢ (𝑧 = 𝑐 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜃 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜏))
7		cbvral8vw.4	. . . 4 ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂))
8	7	4ralbidv 3230	. . 3 ⊢ (𝑤 = 𝑑 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜏 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜂))
9	2, 4, 6, 8	cbvral4vw 3247	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜂)
10		cbvral8vw.5	. . . 4 ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁))
11		cbvral8vw.6	. . . 4 ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜎))
12		cbvral8vw.7	. . . 4 ⊢ (𝑟 = 𝑔 → (𝜎 ↔ 𝜌))
13		cbvral8vw.8	. . . 4 ⊢ (𝑠 = ℎ → (𝜌 ↔ 𝜓))
14	10, 11, 12, 13	cbvral4vw 3247	. . 3 ⊢ (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜂 ↔ ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓)
15	14	4ralbii 3140	. 2 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜂 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓)
16	9, 15	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835  df-ral 3077

This theorem is used by: (None)