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