Description: This implication, proved using only ax-gen and ax-4 on top of
propositional calculus (hence holding, up to the standard interpretation,
in any normal modal logic), shows that the axiom scheme |- E. x T.
implies the axiom scheme |- ( A. x ph -> E. x ph ) . These correspond
to the modal axiom (D), and in predicate calculus, they assert that the
universe of discourse is nonempty. For the converse, see bj-axd2d .
(Contributed by BJ, 16-May-2019)(Proof modification is discouraged.)(New usage is discouraged.)