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 40633. The equivalent of this theorem without the bound variable change is rexlimddv 3290. Version of rexlimddvcbv 40635 with a disjoint variable condition, which does not require ax-13 2389. (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 3447 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜃 ↔ ∃𝑦 ∈ 𝐴 𝜒) |
4 | rexlimddvcbvw.2 | . . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) | |
5 | 4 | rexlimdvaa 3284 | . . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝜒 → 𝜓)) |
6 | 3, 5 | syl5bi 244 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓)) |
7 | 1, 6 | mpd 15 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∈ wcel 2113 ∃wrex 3138 |
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 1969 ax-7 2014 ax-8 2115 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 df-clel 2892 df-ral 3142 df-rex 3143 |
This theorem is referenced by: mnuprdlem1 40683 mnuprdlem2 40684 |
Copyright terms: Public domain | W3C validator |