Add a proof for eximp-surprise2
Add a proof for eximp-surprise2

This adds another proof (eximp-surprise2) that shows, in a different
way, why "there exists" should not normally have implication directly
embedded in it.  This should help people inexperienced with predicate
logic; showing a few proofs of "surprising" results can help them get
a better understanding of what they reall mean.

Signed-off-by: David A. Wheeler <9ae72d22d8b894b865a7a496af4fab6320e6abb2@dwheeler.com>

metamath/set.mm,metamath/set.mm,metamath/set.mm