Definition df-res 4735

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 4725	. 2 class ( A |` B )
4		cvv 2800	. . . 4 class _V
5	2, 4	cxp 4721	. . 3 class ( B X. _V )
6	1, 5	cin 3197	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1395	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  5005  reseq2  5006  nfres  5013  csbresg  5014  res0  5015  opelres  5016  resres  5023  resundi  5024  resundir  5025  resindi  5026  resindir  5027  inres  5028  resdifcom  5029  resiun1  5030  resiun2  5031  resss  5035  ssres  5037  ssres2  5038  relres  5039  xpssres  5046  resopab  5055  ssrnres  5177  imainrect  5180  xpima1  5181  xpima2m  5182  cnvcnv2  5188  resdmres  5226  nfvres  5671  ressnop0  5830