![]() |
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 2374. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvral2vw.1 | ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) |
cbvral2vw.2 | ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvral2vw | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvral2vw.1 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) | |
2 | 1 | ralbidv 3175 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvralvw 3234 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒) |
4 | cbvral2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvralvw 3234 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓) |
6 | 5 | ralbii 3090 | . 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-clel 2813 df-ral 3059 |
This theorem is referenced by: cbvral3vw 3240 cbvral6vw 3242 fununi 6642 fiint 9363 fiintOLD 9364 nqereu 10966 mgmhmpropd 18723 mhmpropd 18817 efgred 19780 mplcoe5 22075 mdetunilem9 22641 fbun 23863 fbunfip 23892 caucfil 25330 pmltpc 25498 negsprop 28081 iscgrglt 28536 axcontlem10 29002 htth 30946 cdj3lem3b 32468 cdj3i 32469 dfmgc2 32970 isros 34148 rossros 34160 fipjust 43554 isotone1 44037 isotone2 44038 ntrclsiso 44056 ntrclskb 44058 ntrclsk3 44059 ntrclsk13 44060 limsuppnfd 45657 pimincfltioo 46673 incsmf 46697 decsmf 46722 catprslem 48798 isthincd2lem1 48826 isthincd2lem2 48835 |
Copyright terms: Public domain | W3C validator |