Theorem rspc8v 3624

Description: 8-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025.)

Hypotheses

Ref	Expression
rspc8v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc8v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
rspc8v.3	⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))
rspc8v.4	⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂))
rspc8v.5	⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁))
rspc8v.6	⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜎))
rspc8v.7	⊢ (𝑟 = 𝐺 → (𝜎 ↔ 𝜌))
rspc8v.8	⊢ (𝑠 = 𝐻 → (𝜌 ↔ 𝜓))

Assertion

Ref	Expression
rspc8v	⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) ∧ ((𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 → 𝜓))

Distinct variable groups:   𝐴,𝑝,𝑞,𝑟,𝑠,𝑤,𝑥,𝑦,𝑧   𝐵,𝑝,𝑞,𝑟,𝑠,𝑤,𝑦,𝑧   𝐶,𝑝,𝑞,𝑟,𝑠,𝑤,𝑧   𝐷,𝑝,𝑞,𝑟,𝑠,𝑤   𝐸,𝑝,𝑞,𝑟,𝑠   𝐹,𝑞,𝑟,𝑠   𝐺,𝑟,𝑠   𝐻,𝑠   𝑥,𝑅   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦,𝑧   𝑤,𝑈,𝑥,𝑦,𝑧   𝑉,𝑝,𝑤,𝑥,𝑦,𝑧   𝑊,𝑝,𝑞,𝑤,𝑥,𝑦,𝑧   𝑋,𝑝,𝑞,𝑟,𝑤,𝑥,𝑦,𝑧   𝑌,𝑝,𝑞,𝑟,𝑠,𝑤,𝑥,𝑦,𝑧   𝜒,𝑥   𝜃,𝑦   𝜏,𝑧   𝜂,𝑤   𝜁,𝑝   𝜎,𝑞   𝜌,𝑟   𝜓,𝑠

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑠,𝑟,𝑞,𝑝)   𝜓(𝑥,𝑦,𝑧,𝑤,𝑟,𝑞,𝑝)   𝜒(𝑦,𝑧,𝑤,𝑠,𝑟,𝑞,𝑝)   𝜃(𝑥,𝑧,𝑤,𝑠,𝑟,𝑞,𝑝)   𝜏(𝑥,𝑦,𝑤,𝑠,𝑟,𝑞,𝑝)   𝜂(𝑥,𝑦,𝑧,𝑠,𝑟,𝑞,𝑝)   𝜁(𝑥,𝑦,𝑧,𝑤,𝑠,𝑟,𝑞)   𝜎(𝑥,𝑦,𝑧,𝑤,𝑠,𝑟,𝑝)   𝜌(𝑥,𝑦,𝑧,𝑤,𝑠,𝑞,𝑝)   𝐵(𝑥)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦,𝑧)   𝑅(𝑦,𝑧,𝑤,𝑠,𝑟,𝑞,𝑝)   𝑆(𝑧,𝑤,𝑠,𝑟,𝑞,𝑝)   𝑇(𝑤,𝑠,𝑟,𝑞,𝑝)   𝑈(𝑠,𝑟,𝑞,𝑝)   𝐸(𝑥,𝑦,𝑧,𝑤)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑝)   𝐺(𝑥,𝑦,𝑧,𝑤,𝑞,𝑝)   𝐻(𝑥,𝑦,𝑧,𝑤,𝑟,𝑞,𝑝)   𝑉(𝑠,𝑟,𝑞)   𝑊(𝑠,𝑟)   𝑋(𝑠)

Proof of Theorem rspc8v

Step	Hyp	Ref	Expression
1		rspc8v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	4ralbidv 3214	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜒))
3		rspc8v.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))
4	3	4ralbidv 3214	. . 3 ⊢ (𝑦 = 𝐵 → (∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜒 ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜃))
5		rspc8v.3	. . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))
6	5	4ralbidv 3214	. . 3 ⊢ (𝑧 = 𝐶 → (∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜃 ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜏))
7		rspc8v.4	. . . 4 ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂))
8	7	4ralbidv 3214	. . 3 ⊢ (𝑤 = 𝐷 → (∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜏 ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜂))
9	2, 4, 6, 8	rspc4v 3622	. 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜂))
10		rspc8v.5	. . 3 ⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁))
11		rspc8v.6	. . 3 ⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜎))
12		rspc8v.7	. . 3 ⊢ (𝑟 = 𝐺 → (𝜎 ↔ 𝜌))
13		rspc8v.8	. . 3 ⊢ (𝑠 = 𝐻 → (𝜌 ↔ 𝜓))
14	10, 11, 12, 13	rspc4v 3622	. 2 ⊢ (((𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌)) → (∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜂 → 𝜓))
15	9, 14	sylan9 507	1 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) ∧ ((𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054

This theorem is referenced by: (None)