![]() |
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 6624 fiint 9324 nqereu 10924 mhmpropd 18678 efgred 19616 mplcoe5 21595 mdetunilem9 22122 fbun 23344 fbunfip 23373 caucfil 24800 pmltpc 24967 negsprop 27509 iscgrglt 27765 axcontlem10 28231 htth 30171 cdj3lem3b 31693 cdj3i 31694 dfmgc2 32166 isros 33166 rossros 33178 fipjust 42316 isotone1 42799 isotone2 42800 ntrclsiso 42818 ntrclskb 42820 ntrclsk3 42821 ntrclsk13 42822 limsuppnfd 44418 pimincfltioo 45434 incsmf 45458 decsmf 45483 mgmhmpropd 46555 catprslem 47630 isthincd2lem1 47647 isthincd2lem2 47656 |
Copyright terms: Public domain | W3C validator |