Theorem bj-dvelimdv 37054

Description: Deduction form of dvelim 2456 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37055. 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 1916 can be replaced with nfal 2329 followed by nfn 1859.

Remark: nfald 2334 uses ax-11 2163; it might be possible to inline and use ax11w 2136 instead, but there is still a use via 19.12 2333 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-dvelimdv.nf	⊢ (𝜑 → Ⅎ𝑥𝜒)
bj-dvelimdv.is	⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
bj-dvelimdv	⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑧   𝜓,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦,𝑧)

Proof of Theorem bj-dvelimdv

Step	Hyp	Ref	Expression
1		bj-dvelimdv.is	. . . 4 ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))
2	1	equsalvw 2006	. . 3 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜒) ↔ 𝜓)
3	2	bicomi 224	. 2 ⊢ (𝜓 ↔ ∀𝑧(𝑧 = 𝑦 → 𝜒))
4		nfv 1916	. . . 4 ⊢ Ⅎ𝑧𝜑
5		nfv 1916	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
6	4, 5	nfan 1901	. . 3 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7		nfeqf2 2382	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
8	7	adantl 481	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9		bj-dvelimdv.nf	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
10	9	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
11	8, 10	nfimd 1896	. . 3 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜒))
12	6, 11	nfald 2334	. 2 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜒))
13	3, 12	nfxfrd 1856	1 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  Ⅎ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 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)