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 2473 with disjoint variable conditions. Uncurried
(imported) form of bj-dvelimdv1 34178. 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 2342 followed by nfn 1857. Remark: nfald 2347 uses ax-11 2161; it might be possible to inline and use ax11w 2134 instead, but there is still a use via 19.12 2346 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 226 | . 2 ⊢ (𝜓 ↔ ∀𝑧(𝑧 = 𝑦 → 𝜒)) |
4 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧𝜑 | |
5 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | |
6 | 4, 5 | nfan 1900 | . . 3 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
7 | nfeqf2 2395 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | |
8 | 7 | adantl 484 | . . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦) |
9 | bj-dvelimdv.nf | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
10 | 9 | adantr 483 | . . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒) |
11 | 8, 10 | nfimd 1895 | . . 3 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜒)) |
12 | 6, 11 | nfald 2347 | . 2 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜒)) |
13 | 3, 12 | nfxfrd 1854 | 1 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-11 2161 ax-12 2177 ax-13 2390 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |