Description: Define the restriction of a class. Definition 6.6(1) of TakeutiZaring
p. 24. For example, the expression ` ( exp |`RR ) (used in
reeff1 ) means "the exponential function e to the x, but the exponent
x must be in the reals" ( df-ef defines the exponential function,
which normally allows the exponent to be a complex number). Another
example is that ( F = { <. 2 , 6 >. , <. 3 , 9 >. }
` /\ B = { 1 , 2 } ) -> ( F |`B ) = { <. 2 , 6 >. } ( ex-res ).
We do not introduce a special syntax for the corestriction of a class:
it will be expressed either as the intersection
( A i^i ( _V X. B ) ) or as the converse of the restricted converse
(see cnvrescnv ). (Contributed by NM, 2-Aug-1994)