Definition df-res 5632

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16082) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16027 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 30531). 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 6149). (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 5622	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3433	. . . 4 class V
5	2, 4	cxp 5618	. . 3 class (𝐵 × V)
6	1, 5	cin 3883	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1548	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5637  reseq1  5931  reseq2  5932  nfres  5939  csbres  5940  res0  5941  dfres3  5942  opelres  5943  resres  5950  resundi  5951  resundir  5952  resindi  5953  resindir  5954  inres  5955  resdifcom  5956  resiun1  5957  resiun2  5958  resss  5959  ssres  5961  ssres2  5962  relres  5963  xpssres  5976  elres  5978  resopab  5992  elrid  6004  imainrect  6135  xpima  6136  cnvcnv2  6147  cnvrescnv  6149  resdmres  6186  resdifdi  6190  resdifdir  6191  ressnop0  7099  fndifnfp  7123  tpres  7148  marypha1lem  9340  gsum2d  19941  gsumxp  19945  pjdm  21685  hausdiag  23631  isngp2  24583  ovoliunlem1  25490  nosupbnd2lem1  27699  noetasuplem3  27719  noetasuplem4  27720  xpdisjres  32689  difres  32691  imadifxp  32692  0res  32694  mbfmcst  34453  0rrv  34645  elrn3  36003  dfon4  36132  bj-opelresdm  37518  bj-idres  37533  bj-elid6  37543  br1cnvres  38654  restrreld  44124  csbresgVD  45351