Definition df-res 4425

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 4415	. 2 class ( A |` B )
4		cvv 2615	. . . 4 class _V
5	2, 4	cxp 4411	. . 3 class ( B X. _V )
6	1, 5	cin 2987	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1287	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4677  reseq2  4678  nfres  4685  csbresg  4686  res0  4687  opelres  4688  resres  4695  resundi  4696  resundir  4697  resindi  4698  resindir  4699  inres  4700  resiun1  4701  resiun2  4702  resss  4706  ssres  4708  ssres2  4709  relres  4710  xpssres  4716  resopab  4725  ssrnres  4841  imainrect  4844  xpima1  4845  xpima2m  4846  cnvcnv2  4852  resdmres  4890  nfvres  5302  ressnop0  5443