Definition df-res 4784

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. }. 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. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-res	|- ( A |` B ) = ( A i^i ( B X. _V ) )

Detailed syntax breakdown of Definition df-res

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cres 4774	. 2 class ( A |` B )
4		cvv 2821	. . . 4 class _V
5	2, 4	cxp 4770	. . 3 class ( B X. _V )
6	1, 5	cin 3219	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1402	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  5055  reseq2  5056  nfres  5063  csbresg  5064  res0  5065  opelres  5066  resres  5073  resundi  5074  resundir  5075  resindi  5076  resindir  5077  inres  5078  resdifcom  5079  resiun1  5080  resiun2  5081  resss  5085  ssres  5087  ssres2  5088  relres  5089  xpssres  5096  resopab  5105  ssrnres  5228  imainrect  5231  xpima1  5232  xpima2m  5233  cnvcnv2  5239  resdmres  5277  nfvres  5729  ressnop0  5890