Definition df-res 5700

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16152) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16099 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 30469). 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 6216). (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 5690	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3477	. . . 4 class V
5	2, 4	cxp 5686	. . 3 class (𝐵 × V)
6	1, 5	cin 3961	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1536	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5705  reseq1  5993  reseq2  5994  nfres  6001  csbres  6002  res0  6003  dfres3  6004  opelres  6005  resres  6012  resundi  6013  resundir  6014  resindi  6015  resindir  6016  inres  6017  resdifcom  6018  resiun1  6019  resiun2  6020  resss  6021  ssres  6023  ssres2  6024  relres  6025  xpssres  6037  elres  6039  resopab  6053  elrid  6065  imainrect  6202  xpima  6203  cnvcnv2  6214  cnvrescnv  6216  resdmres  6253  resdifdi  6257  resdifdir  6258  ressnop0  7172  fndifnfp  7195  tpres  7220  marypha1lem  9470  gsum2d  20004  gsumxp  20008  pjdm  21744  hausdiag  23668  isngp2  24625  ovoliunlem1  25550  nosupbnd2lem1  27774  noetasuplem3  27794  noetasuplem4  27795  xpdisjres  32617  difres  32619  imadifxp  32620  0res  32622  mbfmcst  34240  0rrv  34432  elrn3  35741  dfon4  35874  bj-opelresdm  37127  bj-idres  37142  bj-elid6  37152  br1cnvres  38250  restrreld  43656  csbresgVD  44892