Definition df-res 5659

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16255) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16200 defines the exponential function, which normally allows the exponent to be a complex number). Another example is (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩} (ex-res 30975). We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection (𝐴 ∩ (V × 𝐵)) or as the converse of the restricted converse (see cnvrescnv 6183). (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-res	⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cres 5649	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3450	. . . 4 class V
5	2, 4	cxp 5645	. . 3 class (𝐵 × V)
6	1, 5	cin 3897	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1570	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  inxpssres  5664  reseq1  5960  reseq2  5961  nfres  5968  csbres  5969  res0  5970  dfres3  5971  opelres  5972  resres  5979  resundi  5980  resundir  5981  resindi  5982  resindir  5983  inres  5984  resdifcom  5985  resiun1  5986  resiun2  5987  resss  5988  ssres  5990  ssres2  5991  relres  5992  xpssres  6005  elres  6007  resopab  6024  elrid  6036  imainrect  6168  xpima  6169  cnvcnv2  6180  cnvrescnv  6183  resdmres  6222  resdifdi  6226  resdifdir  6227  ressnop0  7145  fndifnfp  7169  tpres  7195  marypha1lem  9403  gsum2d  20147  gsumxp  20151  pjdm  21974  hausdiag  23925  isngp2  24877  ovoliunlem1  25784  nosupbnd2lem1  28005  noetasuplem3  28025  noetasuplem4  28026  xpdisjres  33125  difres  33127  imadifxp  33128  0res  33130  mbfmcst  34825  0rrv  35017  elrn3  36448  dfon4  36577  bj-opelresdm  37986  bj-idres  38001  bj-elid6  38011  br1cnvres  39126  restrreld  44611  csbresgVD  45821