![]() |
Mathbox for Rohan Ridenour |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rexlimddvcbvw | Structured version Visualization version GIF version |
Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 43696. The equivalent of this theorem without the bound variable change is rexlimddv 3151. Version of rexlimddvcbv 43698 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.) |
Ref | Expression |
---|---|
rexlimddvcbvw.1 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) |
rexlimddvcbvw.2 | ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) |
rexlimddvcbvw.3 | ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexlimddvcbvw | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimddvcbvw.1 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) | |
2 | rexlimddvcbvw.3 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) | |
3 | 2 | cbvrexvw 3226 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜃 ↔ ∃𝑦 ∈ 𝐴 𝜒) |
4 | rexlimddvcbvw.2 | . . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) | |
5 | 4 | rexlimdvaa 3146 | . . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝜒 → 𝜓)) |
6 | 3, 5 | biimtrid 241 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802 df-rex 3061 |
This theorem is referenced by: mnuprdlem1 43770 mnuprdlem2 43771 |
Copyright terms: Public domain | W3C validator |