![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvral2vw | Structured version Visualization version GIF version |
Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3340 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvral2vw.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) |
cbvral2vw.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvral2vw | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvral2vw.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | ralbidv 3171 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvralvw 3224 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒) |
4 | cbvral2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvralvw 3224 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓) |
6 | 5 | ralbii 3093 | . 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2811 df-ral 3062 |
This theorem is referenced by: cbvral3vw 3228 fununi 6577 fiint 9271 nqereu 10870 mhmpropd 18613 efgred 19535 mplcoe5 21457 mdetunilem9 21985 fbun 23207 fbunfip 23236 caucfil 24663 pmltpc 24830 negsprop 27355 iscgrglt 27498 axcontlem10 27964 htth 29902 cdj3lem3b 31424 cdj3i 31425 dfmgc2 31905 isros 32824 rossros 32836 fipjust 41925 isotone1 42408 isotone2 42409 ntrclsiso 42427 ntrclskb 42429 ntrclsk3 42430 ntrclsk13 42431 limsuppnfd 44029 pimincfltioo 45045 incsmf 45069 decsmf 45094 mgmhmpropd 46165 catprslem 47116 isthincd2lem1 47133 isthincd2lem2 47142 |
Copyright terms: Public domain | W3C validator |