![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-dvelimdv | Structured version Visualization version GIF version |
Description: Deduction form of dvelim 2462 with disjoint variable conditions. Uncurried
(imported) form of bj-dvelimdv1 34291. Typically, 𝑧 is a fresh
variable used for the implicit substitution hypothesis that results in
𝜒 (namely, 𝜓 can be thought as 𝜓(𝑥, 𝑦) and 𝜒 as
𝜓(𝑥, 𝑧)). So the theorem says that if x is
effectively free
in 𝜓(𝑥, 𝑧), then if x and y are not the same
variable, then
𝑥 is also effectively free in 𝜓(𝑥, 𝑦), in a context
𝜑.
One can weaken the implicit substitution hypothesis by adding the antecedent 𝜑 but this typically does not make the theorem much more useful. Similarly, one could use nonfreeness hypotheses instead of disjoint variable conditions but since this result is typically used when 𝑧 is a dummy variable, this would not be of much benefit. One could also remove DV (𝑥, 𝑧) since in the proof nfv 1915 can be replaced with nfal 2331 followed by nfn 1858. Remark: nfald 2336 uses ax-11 2158; it might be possible to inline and use ax11w 2131 instead, but there is still a use via 19.12 2335 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-dvelimdv.nf | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
bj-dvelimdv.is | ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
bj-dvelimdv | ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-dvelimdv.is | . . . 4 ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓)) | |
2 | 1 | equsalvw 2010 | . . 3 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜒) ↔ 𝜓) |
3 | 2 | bicomi 227 | . 2 ⊢ (𝜓 ↔ ∀𝑧(𝑧 = 𝑦 → 𝜒)) |
4 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
5 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | |
6 | 4, 5 | nfan 1900 | . . 3 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
7 | nfeqf2 2384 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | |
8 | 7 | adantl 485 | . . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦) |
9 | bj-dvelimdv.nf | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
10 | 9 | adantr 484 | . . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒) |
11 | 8, 10 | nfimd 1895 | . . 3 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜒)) |
12 | 6, 11 | nfald 2336 | . 2 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜒)) |
13 | 3, 12 | nfxfrd 1855 | 1 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1536 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |