Definition df-res 4687

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 4677	. 2 class ( A |` B )
4		cvv 2772	. . . 4 class _V
5	2, 4	cxp 4673	. . 3 class ( B X. _V )
6	1, 5	cin 3165	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1373	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4953  reseq2  4954  nfres  4961  csbresg  4962  res0  4963  opelres  4964  resres  4971  resundi  4972  resundir  4973  resindi  4974  resindir  4975  inres  4976  resdifcom  4977  resiun1  4978  resiun2  4979  resss  4983  ssres  4985  ssres2  4986  relres  4987  xpssres  4994  resopab  5003  ssrnres  5125  imainrect  5128  xpima1  5129  xpima2m  5130  cnvcnv2  5136  resdmres  5174  nfvres  5610  ressnop0  5765