Definition df-res 4413

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 4403	. 2 class ( A |` B )
4		cvv 2612	. . . 4 class _V
5	2, 4	cxp 4399	. . 3 class ( B X. _V )
6	1, 5	cin 2983	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1285	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  4665  reseq2  4666  nfres  4673  csbresg  4674  res0  4675  opelres  4676  resres  4683  resundi  4684  resundir  4685  resindi  4686  resindir  4687  inres  4688  resiun1  4689  resiun2  4690  resss  4694  ssres  4696  ssres2  4697  relres  4698  xpssres  4704  resopab  4713  ssrnres  4827  imainrect  4830  xpima1  4831  xpima2m  4832  cnvcnv2  4838  resdmres  4876  nfvres  5282  ressnop0  5420