Definition df-res 4676

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 4666	. 2 class ( A |` B )
4		cvv 2763	. . . 4 class _V
5	2, 4	cxp 4662	. . 3 class ( B X. _V )
6	1, 5	cin 3156	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1364	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4941  reseq2  4942  nfres  4949  csbresg  4950  res0  4951  opelres  4952  resres  4959  resundi  4960  resundir  4961  resindi  4962  resindir  4963  inres  4964  resdifcom  4965  resiun1  4966  resiun2  4967  resss  4971  ssres  4973  ssres2  4974  relres  4975  xpssres  4982  resopab  4991  ssrnres  5113  imainrect  5116  xpima1  5117  xpima2m  5118  cnvcnv2  5124  resdmres  5162  nfvres  5595  ressnop0  5746