Definition df-res 4730

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 4720	. 2 class ( A |` B )
4		cvv 2799	. . . 4 class _V
5	2, 4	cxp 4716	. . 3 class ( B X. _V )
6	1, 5	cin 3196	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1395	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4998  reseq2  4999  nfres  5006  csbresg  5007  res0  5008  opelres  5009  resres  5016  resundi  5017  resundir  5018  resindi  5019  resindir  5020  inres  5021  resdifcom  5022  resiun1  5023  resiun2  5024  resss  5028  ssres  5030  ssres2  5031  relres  5032  xpssres  5039  resopab  5048  ssrnres  5170  imainrect  5173  xpima1  5174  xpima2m  5175  cnvcnv2  5181  resdmres  5219  nfvres  5662  ressnop0  5819