Definition df-res 5635

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

This definition is referenced by:  inxpssres  5640  reseq1  5928  reseq2  5929  nfres  5936  csbres  5937  res0  5938  dfres3  5939  opelres  5940  resres  5947  resundi  5948  resundir  5949  resindi  5950  resindir  5951  inres  5952  resdifcom  5953  resiun1  5954  resiun2  5955  resss  5956  ssres  5958  ssres2  5959  relres  5960  xpssres  5973  elres  5975  resopab  5989  elrid  6001  imainrect  6134  xpima  6135  cnvcnv2  6146  cnvrescnv  6148  resdmres  6185  resdifdi  6189  resdifdir  6190  ressnop0  7091  fndifnfp  7116  tpres  7141  marypha1lem  9342  gsum2d  19869  gsumxp  19873  pjdm  21632  hausdiag  23548  isngp2  24501  ovoliunlem1  25419  nosupbnd2lem1  27643  noetasuplem3  27663  noetasuplem4  27664  xpdisjres  32560  difres  32562  imadifxp  32563  0res  32565  mbfmcst  34226  0rrv  34418  elrn3  35734  dfon4  35866  bj-opelresdm  37118  bj-idres  37133  bj-elid6  37143  br1cnvres  38243  restrreld  43640  csbresgVD  44868