![]() |
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 3365 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2372. (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 3178 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvralvw 3235 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒) |
4 | cbvral2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvralvw 3235 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓) |
6 | 5 | ralbii 3094 | . 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3062 |
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 3063 |
This theorem is referenced by: cbvral3vw 3241 cbvral6vw 3243 fununi 6621 fiint 9321 nqereu 10921 mhmpropd 18675 efgred 19611 mplcoe5 21587 mdetunilem9 22114 fbun 23336 fbunfip 23365 caucfil 24792 pmltpc 24959 negsprop 27499 iscgrglt 27755 axcontlem10 28221 htth 30159 cdj3lem3b 31681 cdj3i 31682 dfmgc2 32154 isros 33155 rossros 33167 fipjust 42302 isotone1 42785 isotone2 42786 ntrclsiso 42804 ntrclskb 42806 ntrclsk3 42807 ntrclsk13 42808 limsuppnfd 44405 pimincfltioo 45421 incsmf 45445 decsmf 45470 mgmhmpropd 46542 catprslem 47584 isthincd2lem1 47601 isthincd2lem2 47610 |
Copyright terms: Public domain | W3C validator |