Definition df-res 5626

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15920) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15868 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 29006). 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 6127). (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 5616	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3441	. . . 4 class V
5	2, 4	cxp 5612	. . 3 class (𝐵 × V)
6	1, 5	cin 3896	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1540	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5631  reseq1  5911  reseq2  5912  nfres  5919  csbres  5920  res0  5921  dfres3  5922  opelres  5923  resres  5930  resundi  5931  resundir  5932  resindi  5933  resindir  5934  inres  5935  resdifcom  5936  resiun1  5937  resiun2  5938  resss  5942  ssres  5944  ssres2  5945  relres  5946  xpssres  5954  elres  5956  resopab  5968  elrid  5979  imainrect  6113  xpima  6114  cnvcnv2  6125  cnvrescnv  6127  resdmres  6164  resdifdi  6168  resdifdir  6169  ressnop0  7075  fndifnfp  7098  tpres  7126  marypha1lem  9282  gsum2d  19660  gsumxp  19664  pjdm  21012  hausdiag  22894  isngp2  23851  ovoliunlem1  24764  nosupbnd2lem1  26961  noetasuplem3  26981  noetasuplem4  26982  xpdisjres  31137  difres  31139  imadifxp  31140  0res  31143  mbfmcst  32439  0rrv  32631  elrn3  33934  dfon4  34286  bj-opelresdm  35414  bj-idres  35429  bj-elid6  35439  br1cnvres  36527  restrreld  41585  csbresgVD  42825