Definition df-res 5650

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

This definition is referenced by:  inxpssres  5655  reseq1  5944  reseq2  5945  nfres  5952  csbres  5953  res0  5954  dfres3  5955  opelres  5956  resres  5963  resundi  5964  resundir  5965  resindi  5966  resindir  5967  inres  5968  resdifcom  5969  resiun1  5970  resiun2  5971  resss  5972  ssres  5974  ssres2  5975  relres  5976  xpssres  5989  elres  5991  resopab  6005  elrid  6017  imainrect  6154  xpima  6155  cnvcnv2  6166  cnvrescnv  6168  resdmres  6205  resdifdi  6209  resdifdir  6210  ressnop0  7125  fndifnfp  7150  tpres  7175  marypha1lem  9384  gsum2d  19902  gsumxp  19906  pjdm  21616  hausdiag  23532  isngp2  24485  ovoliunlem1  25403  nosupbnd2lem1  27627  noetasuplem3  27647  noetasuplem4  27648  xpdisjres  32527  difres  32529  imadifxp  32530  0res  32532  mbfmcst  34250  0rrv  34442  elrn3  35749  dfon4  35881  bj-opelresdm  37133  bj-idres  37148  bj-elid6  37158  br1cnvres  38258  restrreld  43656  csbresgVD  44884