Definition df-res 5662

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16288) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16233 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 31042). 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 6187). (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 5652	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3450	. . . 4 class V
5	2, 4	cxp 5648	. . 3 class (𝐵 × V)
6	1, 5	cin 4089	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1569	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  inxpssres  5667  reseq1  5963  reseq2  5964  nfres  5971  csbres  5972  res0  5973  dfres3  5974  opelres  5975  resres  5982  resundi  5983  resundir  5984  resindi  5985  resindir  5986  inres  5987  resdifcom  5988  resiun1  5989  resiun2  5990  resss  5991  ssres  5993  ssres2  5994  relres  5995  xpssres  6006  elres  6008  resopab  6025  elrid  6037  imainrect  6172  xpima  6173  cnvcnv2  6184  cnvrescnv  6187  resdmres  6233  resdifdi  6237  resdifdir  6238  ressnop0  7157  fndifnfp  7181  tpres  7207  marypha1lem  9425  gsum2d  20186  gsumxp  20190  pjdm  22013  hausdiag  23964  isngp2  24916  ovoliunlem1  25823  nosupbnd2lem1  28072  noetasuplem3  28092  noetasuplem4  28093  xpdisjres  33234  difres  33236  imadifxp  33237  0res  33239  mbfmcst  34933  0rrv  35125  elrn3  36569  dfon4  36697  bj-opelresdm  38109  bj-idres  38124  bj-elid6  38134  br1cnvres  39249  restrreld  44709  csbresgVD  45919