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 32809
Description: Deduction form of dvelim 2335 with DV conditions. Uncurried (imported) form of bj-dvelimdv 32809. 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 1841 can be replaced with nfal 2151 followed by nfn 1782.

Remark: nfald 2163 uses ax-11 2032; it might be possible to inline and use ax11w 2005 instead, but there is still a use via 19.12 2162 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 1929 . . 3 (∀𝑧(𝑧 = 𝑦𝜒) ↔ 𝜓)
32bicomi 214 . 2 (𝜓 ↔ ∀𝑧(𝑧 = 𝑦𝜒))
4 nfv 1841 . . . 4 𝑧𝜑
5 nfv 1841 . . . 4 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
64, 5nfan 1826 . . 3 𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7 nfeqf2 2295 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
87adantl 482 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9 bj-dvelimdv.nf1 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
109adantr 481 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
118, 10nfimd 1821 . . 3 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦𝜒))
126, 11nfald 2163 . 2 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝑧(𝑧 = 𝑦𝜒))
133, 12nfxfrd 1778 1 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1479  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator