Theorem bj-dvelimdv 37763

Description: Deduction form of dvelim 2480 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37764. 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 1946 can be replaced with nfal 2353 followed by nfn 1889.

Remark: nfald 2358 uses ax-11 2193; it might be possible to inline and use ax11w 2166 instead, but there is still a use via 19.12 2357 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 2036	. . 3 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜒) ↔ 𝜓)
3	2	bicomi 227	. 2 ⊢ (𝜓 ↔ ∀𝑧(𝑧 = 𝑦 → 𝜒))
4		nfv 1946	. . . 4 ⊢ Ⅎ𝑧𝜑
5		nfv 1946	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
6	4, 5	nfan 1931	. . 3 ⊢ Ⅎ𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7		nfeqf2 2406	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
8	7	adantl 487	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9		bj-dvelimdv.nf	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
10	9	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
11	8, 10	nfimd 1926	. . 3 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜒))
12	6, 11	nfald 2358	. 2 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜒))
13	3, 12	nfxfrd 1886	1 ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by: (None)