Definition df-res 5631

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16031) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15976 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 30423). 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 6147). (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 5621	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3437	. . . 4 class V
5	2, 4	cxp 5617	. . 3 class (𝐵 × V)
6	1, 5	cin 3897	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1541	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5636  reseq1  5926  reseq2  5927  nfres  5934  csbres  5935  res0  5936  dfres3  5937  opelres  5938  resres  5945  resundi  5946  resundir  5947  resindi  5948  resindir  5949  inres  5950  resdifcom  5951  resiun1  5952  resiun2  5953  resss  5954  ssres  5956  ssres2  5957  relres  5958  xpssres  5971  elres  5973  resopab  5987  elrid  5999  imainrect  6133  xpima  6134  cnvcnv2  6145  cnvrescnv  6147  resdmres  6184  resdifdi  6188  resdifdir  6189  ressnop0  7092  fndifnfp  7116  tpres  7141  marypha1lem  9324  gsum2d  19886  gsumxp  19890  pjdm  21646  hausdiag  23561  isngp2  24513  ovoliunlem1  25431  nosupbnd2lem1  27655  noetasuplem3  27675  noetasuplem4  27676  xpdisjres  32580  difres  32582  imadifxp  32583  0res  32585  mbfmcst  34293  0rrv  34485  elrn3  35827  dfon4  35956  bj-opelresdm  37210  bj-idres  37225  bj-elid6  37235  br1cnvres  38326  restrreld  43784  csbresgVD  45011