Description: Alternative proof of cbveu . Since df-eu combines two other
quantifiers, one can base this theorem on their associated 'change
bounded variable' kind of theorems as well. (Contributed by Wolf
Lammen, 5-Jan-2023)(Proof modification is discouraged.)(New usage is discouraged.)