Description: Version of dvelimv without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Oct-2002) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)