Definition df-res 5592

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15757) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15705 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 28706). 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 6087). (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 5582	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3422	. . . 4 class V
5	2, 4	cxp 5578	. . 3 class (𝐵 × V)
6	1, 5	cin 3882	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1539	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5597  reseq1  5874  reseq2  5875  nfres  5882  csbres  5883  res0  5884  dfres3  5885  opelres  5886  resres  5893  resundi  5894  resundir  5895  resindi  5896  resindir  5897  inres  5898  resdifcom  5899  resiun1  5900  resiun2  5901  resss  5905  ssres  5907  ssres2  5908  relres  5909  xpssres  5917  elres  5919  resopab  5931  elrid  5942  imainrect  6073  xpima  6074  cnvcnv2  6085  cnvrescnv  6087  resdmres  6124  resdifdi  6128  resdifdir  6129  ressnop0  7007  fndifnfp  7030  tpres  7058  marypha1lem  9122  gsum2d  19488  gsumxp  19492  pjdm  20824  hausdiag  22704  isngp2  23659  ovoliunlem1  24571  xpdisjres  30838  difres  30840  imadifxp  30841  0res  30844  mbfmcst  32126  0rrv  32318  elrn3  33635  nosupbnd2lem1  33845  noetasuplem3  33865  noetasuplem4  33866  dfon4  34122  bj-opelresdm  35243  bj-idres  35258  bj-elid6  35268  restrreld  41164  csbresgVD  42404