Definition df-res 5126

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression ( exp |` RR ) (used in reeff1 14850) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14798 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. } (ex-res 27298). (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 5116	. 2 class ( A |` B )
4		cvv 3200	. . . 4 class _V
5	2, 4	cxp 5112	. . 3 class ( B X. _V )
6	1, 5	cin 3573	. 2 class ( A i^i ( B X. _V ) )
7	3, 6	wceq 1483	1 wff ( A |` B ) = ( A i^i ( B X. _V ) )

This definition is referenced by:  reseq1  5390  reseq2  5391  nfres  5398  csbres  5399  res0  5400  opelres  5401  dfres3  5403  resres  5409  resundi  5410  resundir  5411  resindi  5412  resindir  5413  inres  5414  resdifcom  5415  resiun1  5416  resiun1OLD  5417  resiun2  5418  resss  5422  ssres  5424  ssres2  5425  relres  5426  xpssres  5434  resopab  5446  ssrnres  5572  imainrect  5575  xpima  5576  cnvcnv2  5588  resdmres  5625  ressnop0  6420  fndifnfp  6442  tpres  6466  marypha1lem  8339  gsum2d  18371  gsumxp  18375  pjdm  20051  hausdiag  21448  isngp2  22401  ovoliunlem1  23270  xpdisjres  29411  difres  29413  imadifxp  29414  mbfmcst  30321  0rrv  30513  elrn3  31652  nosupbnd2lem1  31861  noetalem2  31864  noetalem3  31865  dfon4  32000  opelresALTV  34031  inxpssres  34076  restrreld  37959  csbresgOLD  39055  csbresgVD  39131