Definition df-res 5628

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

This definition is referenced by:  inxpssres  5633  reseq1  5922  reseq2  5923  nfres  5930  csbres  5931  res0  5932  dfres3  5933  opelres  5934  resres  5941  resundi  5942  resundir  5943  resindi  5944  resindir  5945  inres  5946  resdifcom  5947  resiun1  5948  resiun2  5949  resss  5950  ssres  5952  ssres2  5953  relres  5954  xpssres  5967  elres  5969  resopab  5983  elrid  5995  imainrect  6128  xpima  6129  cnvcnv2  6140  cnvrescnv  6142  resdmres  6179  resdifdi  6183  resdifdir  6184  ressnop0  7086  fndifnfp  7110  tpres  7135  marypha1lem  9317  gsum2d  19882  gsumxp  19886  pjdm  21642  hausdiag  23558  isngp2  24510  ovoliunlem1  25428  nosupbnd2lem1  27652  noetasuplem3  27672  noetasuplem4  27673  xpdisjres  32573  difres  32575  imadifxp  32576  0res  32578  mbfmcst  34267  0rrv  34459  elrn3  35794  dfon4  35926  bj-opelresdm  37178  bj-idres  37193  bj-elid6  37203  br1cnvres  38303  restrreld  43699  csbresgVD  44926