Description: This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A. x x = y as an antecedent. ph normally has z free and can be read ph ( z ) , and ps substitutes y for z and can be read ph ( y ) . We do not require that x and y be distinct: if they are not, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with A. x A. z , conjoin them, and apply dvelimdf .
Other variants of this theorem are dvelimh (with no distinct variable restrictions) and dvelimhw (that avoids ax-13 ). Usage of this theorem is discouraged because it depends on ax-13 . Check out dvelimhw for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dvelim.1 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| dvelim.2 | ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | dvelim | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dvelim.1 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| 2 | dvelim.2 | ⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 3 | ax-5 | ⊢ ( 𝜓 → ∀ 𝑧 𝜓 ) | |
| 4 | 1 3 2 | dvelimh | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) |