Theorem bj-dvelimdv 37514

Description: Deduction form of dvelim 2483 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37515. 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 1944 can be replaced with nfal 2356 followed by nfn 1887.

Remark: nfald 2361 uses ax-11 2192; it might be possible to inline and use ax11w 2165 instead, but there is still a use via 19.12 2360 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 2034	. . 3 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜒) ↔ 𝜓)
3	2	bicomi 227	. 2 ⊢ (𝜓 ↔ ∀𝑧(𝑧 = 𝑦 → 𝜒))
4		nfv 1944	. . . 4 ⊢ Ⅎ𝑧𝜑
5		nfv 1944	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
6	4, 5	nfan 1929	. . 3 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7		nfeqf2 2409	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
8	7	adantl 486	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9		bj-dvelimdv.nf	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
10	9	adantr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
11	8, 10	nfimd 1924	. . 3 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜒))
12	6, 11	nfald 2361	. 2 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜒))
13	3, 12	nfxfrd 1884	1 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568  Ⅎwnf 1813

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213  ax-13 2404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814

This theorem is used by: (None)