Axiom of existence (intuitionistic logic axiom ax-i9). In classical logic, this is equivalent to [ax-6] but in intuitionistic logic it needs to be stated using the existential quantifier. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)