Description: Define restricted existential quantification. Special case of Definition
4.15(4) of TakeutiZaring p. 22.

Note: This notation is most often used to express that ph holds for
at least one element of a given class A . For this reading
F/_ x A is required, though, for example, asserted when x and
A are disjoint.

Should instead A depend on x , you rather assert at least one
x fulfilling ph happens to be contained in the corresponding
A ( x ) . This interpretation is rarely needed (see also df-ral ).
(Contributed by NM, 30-Aug-1993)