| 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 3368 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2377. (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 3178 | . . 3 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
| 3 | 2 | cbvralvw 3237 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒) |
| 4 | cbvral2vw.2 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) | |
| 5 | 4 | cbvralvw 3237 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑤 ∈ 𝐵 𝜓) |
| 6 | 5 | ralbii 3093 | . 2 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
| 7 | 3, 6 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 df-ral 3062 |
| This theorem is referenced by: cbvral3vw 3243 cbvral6vw 3245 fununi 6641 fiint 9366 fiintOLD 9367 nqereu 10969 mgmhmpropd 18711 mhmpropd 18805 efgred 19766 mplcoe5 22058 mdetunilem9 22626 fbun 23848 fbunfip 23877 caucfil 25317 pmltpc 25485 negsprop 28067 iscgrglt 28522 axcontlem10 28988 htth 30937 cdj3lem3b 32459 cdj3i 32460 dfmgc2 32986 isros 34169 rossros 34181 fipjust 43578 isotone1 44061 isotone2 44062 ntrclsiso 44080 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 limsuppnfd 45717 pimincfltioo 46733 incsmf 46757 decsmf 46782 catprslem 48899 isthincd2lem1 49075 isthincd2lem2 49084 |
| Copyright terms: Public domain | W3C validator |