Definition df-res 4551

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 4541	. 2 class ( A |` B )
4		cvv 2686	. . . 4 class _V
5	2, 4	cxp 4537	. . 3 class ( B X. _V )
6	1, 5	cin 3070	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1331	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4813  reseq2  4814  nfres  4821  csbresg  4822  res0  4823  opelres  4824  resres  4831  resundi  4832  resundir  4833  resindi  4834  resindir  4835  inres  4836  resdifcom  4837  resiun1  4838  resiun2  4839  resss  4843  ssres  4845  ssres2  4846  relres  4847  xpssres  4854  resopab  4863  ssrnres  4981  imainrect  4984  xpima1  4985  xpima2m  4986  cnvcnv2  4992  resdmres  5030  nfvres  5454  ressnop0  5601