Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-dvelimdv Structured version   Visualization version   GIF version

Theorem bj-dvelimdv 33328
Description: Deduction form of dvelim 2458 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 33329. 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 non-freeness 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(x,z) since in the proof nfv 2010 can be replaced with nfal 2346 followed by nfn 1954.

Remark: nfald 2351 uses ax-11 2200; it might be possible to inline and use ax11w 2174 instead, but there is still a use via 19.12 2350 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
StepHypRef Expression
1 bj-dvelimdv.is . . . 4 (𝑧 = 𝑦 → (𝜒𝜓))
21equsalvw 2103 . . 3 (∀𝑧(𝑧 = 𝑦𝜒) ↔ 𝜓)
32bicomi 216 . 2 (𝜓 ↔ ∀𝑧(𝑧 = 𝑦𝜒))
4 nfv 2010 . . . 4 𝑧𝜑
5 nfv 2010 . . . 4 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
64, 5nfan 1999 . . 3 𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7 nfeqf2 2382 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
87adantl 474 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9 bj-dvelimdv.nf . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
109adantr 473 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
118, 10nfimd 1993 . . 3 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦𝜒))
126, 11nfald 2351 . 2 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝑧(𝑧 = 𝑦𝜒))
133, 12nfxfrd 1950 1 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wal 1651  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator