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 33140
Description: Deduction form of dvelim 2477 with DV conditions. Uncurried (imported) form of bj-dvelimdv 33140. 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 weakend 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 DV 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(z,x) since in the proof nfv 1992 can be replaced with nfal 2300 followed by nfn 1933.

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

Hypotheses
Ref Expression
bj-dvelimdv.nf 𝑥𝜑
bj-dvelimdv.nf1 (𝜑 → Ⅎ𝑥𝜒)
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 2086 . . 3 (∀𝑧(𝑧 = 𝑦𝜒) ↔ 𝜓)
32bicomi 214 . 2 (𝜓 ↔ ∀𝑧(𝑧 = 𝑦𝜒))
4 nfv 1992 . . . 4 𝑧𝜑
5 nfv 1992 . . . 4 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
64, 5nfan 1977 . . 3 𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7 nfeqf2 2442 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
87adantl 473 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9 bj-dvelimdv.nf1 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
109adantr 472 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
118, 10nfimd 1972 . . 3 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦𝜒))
126, 11nfald 2310 . 2 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝑧(𝑧 = 𝑦𝜒))
133, 12nfxfrd 1929 1 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1630  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator