MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvral8vw Structured version   Visualization version   GIF version

Theorem cbvral8vw 3242
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
StepHypRef Expression
1 cbvral8vw.1 . . . 4 (𝑥 = 𝑎 → (𝜑𝜒))
214ralbidv 3221 . . 3 (𝑥 = 𝑎 → (∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜑 ↔ ∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜒))
3 cbvral8vw.2 . . . 4 (𝑦 = 𝑏 → (𝜒𝜃))
434ralbidv 3221 . . 3 (𝑦 = 𝑏 → (∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜒 ↔ ∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜃))
5 cbvral8vw.3 . . . 4 (𝑧 = 𝑐 → (𝜃𝜏))
654ralbidv 3221 . . 3 (𝑧 = 𝑐 → (∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜃 ↔ ∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜏))
7 cbvral8vw.4 . . . 4 (𝑤 = 𝑑 → (𝜏𝜂))
874ralbidv 3221 . . 3 (𝑤 = 𝑑 → (∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜏 ↔ ∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜂))
92, 4, 6, 8cbvral4vw 3240 . 2 (∀𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜑 ↔ ∀𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜂)
10 cbvral8vw.5 . . . 4 (𝑝 = 𝑒 → (𝜂𝜁))
11 cbvral8vw.6 . . . 4 (𝑞 = 𝑓 → (𝜁𝜎))
12 cbvral8vw.7 . . . 4 (𝑟 = 𝑔 → (𝜎𝜌))
13 cbvral8vw.8 . . . 4 (𝑠 = → (𝜌𝜓))
1410, 11, 12, 13cbvral4vw 3240 . . 3 (∀𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜂 ↔ ∀𝑒𝐸𝑓𝐹𝑔𝐺𝐻 𝜓)
15144ralbii 3130 . 2 (∀𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜂 ↔ ∀𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷𝑒𝐸𝑓𝐹𝑔𝐺𝐻 𝜓)
169, 15bitri 274 1 (∀𝑥𝐴𝑦𝐵𝑧𝐶𝑤𝐷𝑝𝐸𝑞𝐹𝑟𝐺𝑠𝐻 𝜑 ↔ ∀𝑎𝐴𝑏𝐵𝑐𝐶𝑑𝐷𝑒𝐸𝑓𝐹𝑔𝐺𝐻 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2809  df-ral 3061
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator