df-∃mo

Definition.

Arguments:

x (sv), phi (pr),

Assertions:

(_em1xphileftrightarrow(existsxphito_e1xphi))