![]() |
Mathbox for Rohan Ridenour |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rexlimddvcbv | Structured version Visualization version GIF version |
Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44195. The equivalent of this theorem without the bound variable change is rexlimddv 3159. Usage of this theorem is discouraged because it depends on ax-13 2375, see rexlimddvcbvw 44196 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
Ref | Expression |
---|---|
rexlimddvcbv.1 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) |
rexlimddvcbv.2 | ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) |
rexlimddvcbv.3 | ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexlimddvcbv | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimddvcbv.1 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃) | |
2 | rexlimddvcbv.3 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒)) | |
3 | rexlimddvcbv.2 | . . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓) | |
4 | 2, 3 | rexlimdvaacbv 44195 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2106 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-10 2139 ax-11 2155 ax-12 2175 ax-13 2375 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clel 2814 df-nfc 2890 df-ral 3060 df-rex 3069 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |