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

Note: This notation is most often used to express that ph holds for
all elements 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 focus on those x
that happen to be contained in the corresponding A ( x ) . This
hardly used interpretation could still occur naturally. For some
examples, look at ralndv1 or ralndv2 , courtesy of AV.

So be careful to either keep A independent of x , or adjust your
comments to include such exotic cases. (Contributed by NM, 19-Aug-1993)