Definition df-res

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 ( 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)

	Ref	Expression
Assertion	df-res	$$⊢{A\upharpoonright }_B=A\cap \left(B\times \mathrm{V}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cres	$$class\left({A\upharpoonright }_B\right)$$
3		cvv	$$class\mathrm{V}$$
4	1 3	cxp	$$class\left(B\times \mathrm{V}\right)$$
5	0 4	cin	$$class\left(A\cap \left(B\times \mathrm{V}\right)\right)$$
6	2 5	wceq	$$wff{A\upharpoonright }_B=A\cap \left(B\times \mathrm{V}\right)$$