![]() |
Mathbox for BTernaryTau |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvelimalcased | Structured version Visualization version GIF version |
Description: Eliminate a disjoint variable condition from a universally quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.) |
Ref | Expression |
---|---|
dvelimalcased.1 | ⊢ Ⅎ𝑥𝜑 |
dvelimalcased.2 | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) |
dvelimalcased.3 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
dvelimalcased.4 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) |
dvelimalcased.5 | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) |
dvelimalcased.6 | ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) |
dvelimalcased.7 | ⊢ (𝜑 → ∀𝑧𝜓) |
dvelimalcased.8 | ⊢ (𝜑 → ∀𝑥𝜒) |
Ref | Expression |
---|---|
dvelimalcased | ⊢ (𝜑 → ∀𝑥𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvelimalcased.8 | . . 3 ⊢ (𝜑 → ∀𝑥𝜒) | |
2 | dvelimalcased.1 | . . . . . 6 ⊢ Ⅎ𝑥𝜑 | |
3 | nfa1 2147 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑦 | |
4 | 2, 3 | nfan 1898 | . . . . 5 ⊢ Ⅎ𝑥(𝜑 ∧ ∀𝑥 𝑥 = 𝑦) |
5 | dvelimalcased.6 | . . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃)) | |
6 | 4, 5 | alimd 2208 | . . . 4 ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (∀𝑥𝜒 → ∀𝑥𝜃)) |
7 | 6 | ex 412 | . . 3 ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜒 → ∀𝑥𝜃))) |
8 | 1, 7 | mpid 44 | . 2 ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → ∀𝑥𝜃)) |
9 | dvelimalcased.7 | . . 3 ⊢ (𝜑 → ∀𝑧𝜓) | |
10 | nfv 1913 | . . . . . 6 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | |
11 | dvelimalcased.2 | . . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | |
12 | 10, 11 | nfan1c 35041 | . . . . 5 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
13 | nfna1 2148 | . . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦 | |
14 | 2, 13 | nfan 1898 | . . . . 5 ⊢ Ⅎ𝑥(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
15 | dvelimalcased.3 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) | |
16 | dvelimalcased.4 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) | |
17 | dvelimalcased.5 | . . . . 5 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃))) | |
18 | 12, 14, 15, 16, 17 | cbv1v 2335 | . . . 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 Ⅎ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: dvelimalcasei 35044 |
Copyright terms: Public domain | W3C validator |