Prove ⊢ x ∉ s ⇒ s DELETE x = s and export as a rewrite

It turns out that the implication can be an iff (which is the existing
DELETE_NOT_ELEMENT theorem), but this is less useful for most
simplification.
Export pred_setTheory's BIJ_EMPTY as an automatic rewrite.