Definition df-res 4700

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 4690	. 2 class ( A |` B )
4		cvv 2773	. . . 4 class _V
5	2, 4	cxp 4686	. . 3 class ( B X. _V )
6	1, 5	cin 3169	. 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  4967  reseq2  4968  nfres  4975  csbresg  4976  res0  4977  opelres  4978  resres  4985  resundi  4986  resundir  4987  resindi  4988  resindir  4989  inres  4990  resdifcom  4991  resiun1  4992  resiun2  4993  resss  4997  ssres  4999  ssres2  5000  relres  5001  xpssres  5008  resopab  5017  ssrnres  5139  imainrect  5142  xpima1  5143  xpima2m  5144  cnvcnv2  5150  resdmres  5188  nfvres  5628  ressnop0  5783