Definition df-res 5676

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16178) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16123 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 30735). 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 6197). (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 5666	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3463	. . . 4 class V
5	2, 4	cxp 5662	. . 3 class (𝐵 × V)
6	1, 5	cin 3912	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1567	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5681  reseq1  5975  reseq2  5976  nfres  5983  csbres  5984  res0  5985  dfres3  5986  opelres  5987  resres  5994  resundi  5995  resundir  5996  resindi  5997  resindir  5998  inres  5999  resdifcom  6000  resiun1  6001  resiun2  6002  resss  6003  ssres  6005  ssres2  6006  relres  6007  xpssres  6020  elres  6022  resopab  6039  elrid  6051  imainrect  6182  xpima  6183  cnvcnv2  6194  cnvrescnv  6197  resdmres  6236  resdifdi  6240  resdifdir  6241  ressnop0  7153  fndifnfp  7177  tpres  7202  marypha1lem  9395  gsum2d  20044  gsumxp  20048  pjdm  21828  hausdiag  23773  isngp2  24725  ovoliunlem1  25632  nosupbnd2lem1  27847  noetasuplem3  27867  noetasuplem4  27868  xpdisjres  32886  difres  32888  imadifxp  32889  0res  32891  mbfmcst  34596  0rrv  34788  elrn3  36189  dfon4  36318  bj-opelresdm  37714  bj-idres  37729  bj-elid6  37739  br1cnvres  38850  restrreld  44322  csbresgVD  45532