Definition df-res 4489

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 >. } . (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 4479	. 2 class ( A |` B )
4		cvv 2641	. . . 4 class _V
5	2, 4	cxp 4475	. . 3 class ( B X. _V )
6	1, 5	cin 3020	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1299	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4749  reseq2  4750  nfres  4757  csbresg  4758  res0  4759  opelres  4760  resres  4767  resundi  4768  resundir  4769  resindi  4770  resindir  4771  inres  4772  resdifcom  4773  resiun1  4774  resiun2  4775  resss  4779  ssres  4781  ssres2  4782  relres  4783  xpssres  4790  resopab  4799  ssrnres  4917  imainrect  4920  xpima1  4921  xpima2m  4922  cnvcnv2  4928  resdmres  4966  nfvres  5386  ressnop0  5533