Note: This notation is most often used to express that ph holds for
exactly 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 exactly 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, 22-Nov-1994)