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 3464 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 10-Aug-2004.) (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 3197 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | cbvralvw 3449 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒) |
4 | cbvral2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
5 | 4 | cbvralvw 3449 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓) |
6 | 5 | ralbii 3165 | . 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
7 | 3, 6 | bitri 277 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-clel 2893 df-ral 3143 |
This theorem is referenced by: cbvral3vw 3463 fununi 6429 fiint 8795 nqereu 10351 mhmpropd 17962 efgred 18874 mplcoe5 20249 mdetunilem9 21229 fbun 22448 fbunfip 22477 caucfil 23886 pmltpc 24051 iscgrglt 26300 axcontlem10 26759 htth 28695 cdj3lem3b 30217 cdj3i 30218 isros 31427 rossros 31439 fipjust 39973 isotone1 40447 isotone2 40448 ntrclsiso 40466 ntrclskb 40468 ntrclsk3 40469 ntrclsk13 40470 limsuppnfd 42032 pimincfltioo 43045 incsmf 43068 decsmf 43092 mgmhmpropd 44101 |
Copyright terms: Public domain | W3C validator |