Definition df-res 5646

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

This definition is referenced by:  inxpssres  5651  reseq1  5942  reseq2  5943  nfres  5950  csbres  5951  res0  5952  dfres3  5953  opelres  5954  resres  5961  resundi  5962  resundir  5963  resindi  5964  resindir  5965  inres  5966  resdifcom  5967  resiun1  5968  resiun2  5969  resss  5970  ssres  5972  ssres2  5973  relres  5974  xpssres  5987  elres  5989  resopab  6003  elrid  6015  imainrect  6149  xpima  6150  cnvcnv2  6161  cnvrescnv  6163  resdmres  6200  resdifdi  6204  resdifdir  6205  ressnop0  7110  fndifnfp  7134  tpres  7159  marypha1lem  9350  gsum2d  19918  gsumxp  19922  pjdm  21679  hausdiag  23606  isngp2  24558  ovoliunlem1  25476  nosupbnd2lem1  27700  noetasuplem3  27720  noetasuplem4  27721  xpdisjres  32691  difres  32693  imadifxp  32694  0res  32696  mbfmcst  34443  0rrv  34635  elrn3  35984  dfon4  36113  bj-opelresdm  37427  bj-idres  37442  bj-elid6  37452  br1cnvres  38554  restrreld  44052  csbresgVD  45279