Definition df-res 4640

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 4630	. 2 class ( A |` B )
4		cvv 2739	. . . 4 class _V
5	2, 4	cxp 4626	. . 3 class ( B X. _V )
6	1, 5	cin 3130	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1353	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4903  reseq2  4904  nfres  4911  csbresg  4912  res0  4913  opelres  4914  resres  4921  resundi  4922  resundir  4923  resindi  4924  resindir  4925  inres  4926  resdifcom  4927  resiun1  4928  resiun2  4929  resss  4933  ssres  4935  ssres2  4936  relres  4937  xpssres  4944  resopab  4953  ssrnres  5073  imainrect  5076  xpima1  5077  xpima2m  5078  cnvcnv2  5084  resdmres  5122  nfvres  5550  ressnop0  5699