Description: Deduction form of dvelim with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 . Typically, z is a fresh variable used for the implicit substitution hypothesis that results in ch (namely, ps can be thought as ps ( x , y ) and ch as ps ( x , z ) ). So the theorem says that if x is effectively free in ps ( x , z ) , then if x and y are not the same variable, then x is also effectively free in ps ( x , y ) , in a context ph .
One can weaken the implicit substitution hypothesis by adding the antecedent ph 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 z is a dummy variable, this would not be of much benefit. One could also remove DV ( x , z ) since in the proof nfv can be replaced with nfal followed by nfn .
Remark: nfald uses ax-11 ; it might be possible to inline and use ax11w instead, but there is still a use via 19.12 anyway. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-dvelimdv.nf | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | |
| bj-dvelimdv.is | ⊢ ( 𝑧 = 𝑦 → ( 𝜒 ↔ 𝜓 ) ) | ||
| Assertion | bj-dvelimdv | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-dvelimdv.nf | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 ) | |
| 2 | bj-dvelimdv.is | ⊢ ( 𝑧 = 𝑦 → ( 𝜒 ↔ 𝜓 ) ) | |
| 3 | 2 | equsalvw | ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) ↔ 𝜓 ) |
| 4 | 3 | bicomi | ⊢ ( 𝜓 ↔ ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) ) |
| 5 | nfv | ⊢ Ⅎ 𝑧 𝜑 | |
| 6 | nfv | ⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 | |
| 7 | 5 6 | nfan | ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) |
| 8 | nfeqf2 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 ) | |
| 9 | 8 | adantl | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑧 = 𝑦 ) |
| 10 | 1 | adantr | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜒 ) |
| 11 | 9 10 | nfimd | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜒 ) ) |
| 12 | 7 11 | nfald | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜒 ) ) |
| 13 | 4 12 | nfxfrd | ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 ) |