Title: Decision procedures for elementary sublanguages of set theory.  VII. Validity in set theory when a choice operator is present