Definition df-res 4686

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 4676	. 2 class ( A |` B )
4		cvv 2771	. . . 4 class _V
5	2, 4	cxp 4672	. . 3 class ( B X. _V )
6	1, 5	cin 3164	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1372	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4952  reseq2  4953  nfres  4960  csbresg  4961  res0  4962  opelres  4963  resres  4970  resundi  4971  resundir  4972  resindi  4973  resindir  4974  inres  4975  resdifcom  4976  resiun1  4977  resiun2  4978  resss  4982  ssres  4984  ssres2  4985  relres  4986  xpssres  4993  resopab  5002  ssrnres  5124  imainrect  5127  xpima1  5128  xpima2m  5129  cnvcnv2  5135  resdmres  5173  nfvres  5609  ressnop0  5764