Definition df-res 5632

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16076) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16021 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 30499). 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 6148). (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 5622	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3427	. . . 4 class V
5	2, 4	cxp 5618	. . 3 class (𝐵 × V)
6	1, 5	cin 3884	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1542	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5637  reseq1  5927  reseq2  5928  nfres  5935  csbres  5936  res0  5937  dfres3  5938  opelres  5939  resres  5946  resundi  5947  resundir  5948  resindi  5949  resindir  5950  inres  5951  resdifcom  5952  resiun1  5953  resiun2  5954  resss  5955  ssres  5957  ssres2  5958  relres  5959  xpssres  5972  elres  5974  resopab  5988  elrid  6000  imainrect  6134  xpima  6135  cnvcnv2  6146  cnvrescnv  6148  resdmres  6185  resdifdi  6189  resdifdir  6190  ressnop0  7096  fndifnfp  7120  tpres  7145  marypha1lem  9335  gsum2d  19936  gsumxp  19940  pjdm  21676  hausdiag  23598  isngp2  24550  ovoliunlem1  25457  nosupbnd2lem1  27667  noetasuplem3  27687  noetasuplem4  27688  xpdisjres  32656  difres  32658  imadifxp  32659  0res  32661  mbfmcst  34391  0rrv  34583  elrn3  35932  dfon4  36061  bj-opelresdm  37447  bj-idres  37462  bj-elid6  37472  br1cnvres  38583  restrreld  44082  csbresgVD  45309