![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvral6vw | Structured version Visualization version GIF version |
Description: Change bound variables of sextuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 5-Mar-2025.) |
Ref | Expression |
---|---|
cbvral6vw.1 | ⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒)) |
cbvral6vw.2 | ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃)) |
cbvral6vw.3 | ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏)) |
cbvral6vw.4 | ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂)) |
cbvral6vw.5 | ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁)) |
cbvral6vw.6 | ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvral6vw | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvral6vw.1 | . . . 4 ⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒)) | |
2 | 1 | 2ralbidv 3217 | . . 3 ⊢ (𝑥 = 𝑎 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒)) |
3 | cbvral6vw.2 | . . . 4 ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃)) | |
4 | 3 | 2ralbidv 3217 | . . 3 ⊢ (𝑦 = 𝑏 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜃)) |
5 | cbvral6vw.3 | . . . 4 ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏)) | |
6 | 5 | 2ralbidv 3217 | . . 3 ⊢ (𝑧 = 𝑐 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜃 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜏)) |
7 | cbvral6vw.4 | . . . 4 ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂)) | |
8 | 7 | 2ralbidv 3217 | . . 3 ⊢ (𝑤 = 𝑑 → (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜏 ↔ ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂)) |
9 | 2, 4, 6, 8 | cbvral4vw 3240 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂) |
10 | cbvral6vw.5 | . . . 4 ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁)) | |
11 | cbvral6vw.6 | . . . 4 ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓)) | |
12 | 10, 11 | cbvral2vw 3237 | . . 3 ⊢ (∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂 ↔ ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓) |
13 | 12 | 4ralbii 3130 | . 2 ⊢ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜂 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓) |
14 | 9, 13 | bitri 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: mulsproplemcbv 27481 mulsprop 27496 |
Copyright terms: Public domain | W3C validator |