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 16029) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15974 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 30385). 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 6144). (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 3436	. . . 4 class V
5	2, 4	cxp 5617	. . 3 class (𝐵 × V)
6	1, 5	cin 3902	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1540	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5636  reseq1  5924  reseq2  5925  nfres  5932  csbres  5933  res0  5934  dfres3  5935  opelres  5936  resres  5943  resundi  5944  resundir  5945  resindi  5946  resindir  5947  inres  5948  resdifcom  5949  resiun1  5950  resiun2  5951  resss  5952  ssres  5954  ssres2  5955  relres  5956  xpssres  5969  elres  5971  resopab  5985  elrid  5997  imainrect  6130  xpima  6131  cnvcnv2  6142  cnvrescnv  6144  resdmres  6181  resdifdi  6185  resdifdir  6186  ressnop0  7087  fndifnfp  7112  tpres  7137  marypha1lem  9323  gsum2d  19851  gsumxp  19855  pjdm  21614  hausdiag  23530  isngp2  24483  ovoliunlem1  25401  nosupbnd2lem1  27625  noetasuplem3  27645  noetasuplem4  27646  xpdisjres  32542  difres  32544  imadifxp  32545  0res  32547  mbfmcst  34233  0rrv  34425  elrn3  35745  dfon4  35877  bj-opelresdm  37129  bj-idres  37144  bj-elid6  37154  br1cnvres  38254  restrreld  43650  csbresgVD  44878