![]() |
Mathbox for BTernaryTau |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvelimexcased | Structured version Visualization version GIF version |
Description: Eliminate a disjoint variable condition from an existentially quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.) |
Ref | Expression |
---|---|
dvelimexcased.1 | ⊢ Ⅎ𝑥𝜑 |
dvelimexcased.2 | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) |
dvelimexcased.3 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
dvelimexcased.4 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) |
dvelimexcased.5 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) |
dvelimexcased.6 | ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) |
dvelimexcased.7 | ⊢ (𝜑 → ∃𝑧𝜓) |
dvelimexcased.8 | ⊢ (𝜑 → ∃𝑥𝜒) |
Ref | Expression |
---|---|
dvelimexcased | ⊢ (𝜑 → ∃𝑥𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvelimexcased.8 | . . 3 ⊢ (𝜑 → ∃𝑥𝜒) | |
2 | dvelimexcased.1 | . . . . . 6 ⊢ Ⅎ𝑥𝜑 | |
3 | nfa1 2147 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑦 | |
4 | 2, 3 | nfan 1898 | . . . . 5 ⊢ Ⅎ𝑥(𝜑 ∧ ∀𝑥 𝑥 = 𝑦) |
5 | dvelimexcased.6 | . . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) | |
6 | 4, 5 | eximd 2212 | . . . 4 ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (∃𝑥𝜒 → ∃𝑥𝜃)) |
7 | 6 | ex 412 | . . 3 ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜒 → ∃𝑥𝜃))) |
8 | 1, 7 | mpid 44 | . 2 ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝜃)) |
9 | dvelimexcased.7 | . . 3 ⊢ (𝜑 → ∃𝑧𝜓) | |
10 | nfv 1913 | . . . . . 6 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | |
11 | dvelimexcased.2 | . . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | |
12 | 10, 11 | nfan1c 35041 | . . . . 5 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
13 | nfna1 2148 | . . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦 | |
14 | 2, 13 | nfan 1898 | . . . . 5 ⊢ Ⅎ𝑥(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
15 | dvelimexcased.3 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) | |
16 | dvelimexcased.4 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) | |
17 | dvelimexcased.5 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) | |
18 | 12, 14, 15, 16, 17 | cbvex1v 35042 | . . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∃𝑧𝜓 → ∃𝑥𝜃)) |
19 | 18 | ex 412 | . . 3 ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜓 → ∃𝑥𝜃))) |
20 | 9, 19 | mpid 44 | . 2 ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝜃)) |
21 | 8, 20 | pm2.61d 179 | 1 ⊢ (𝜑 → ∃𝑥𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∀wal 1535 ∃wex 1777 Ⅎwnf 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-10 2136 ax-11 2153 ax-12 2173 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-tru 1540 df-ex 1778 df-nf 1782 |
This theorem is referenced by: dvelimexcasei 35046 |
Copyright terms: Public domain | W3C validator |