Description: Obsolete version of moimi as of 9-May-2023. The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006) (Proof modification is discouraged.) (New usage is discouraged.)