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 34194
 Description: Deduction form of dvelim 2475 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 34195. 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 1916 can be replaced with nfal 2344 followed by nfn 1858. Remark: nfald 2349 uses ax-11 2162; it might be possible to inline and use ax11w 2135 instead, but there is still a use via 19.12 2348 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 2011 . . 3 (∀𝑧(𝑧 = 𝑦𝜒) ↔ 𝜓)
32bicomi 227 . 2 (𝜓 ↔ ∀𝑧(𝑧 = 𝑦𝜒))
4 nfv 1916 . . . 4 𝑧𝜑
5 nfv 1916 . . . 4 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
64, 5nfan 1901 . . 3 𝑧(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
7 nfeqf2 2397 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
87adantl 485 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑧 = 𝑦)
9 bj-dvelimdv.nf . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
109adantr 484 . . . 4 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜒)
118, 10nfimd 1896 . . 3 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦𝜒))
126, 11nfald 2349 . 2 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝑧(𝑧 = 𝑦𝜒))
133, 12nfxfrd 1855 1 ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-11 2162  ax-12 2179  ax-13 2392 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator