Definition df-res 5563

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15681) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15629 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 28524). 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 6058). (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 5553	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3408	. . . 4 class V
5	2, 4	cxp 5549	. . 3 class (𝐵 × V)
6	1, 5	cin 3865	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1543	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5568  reseq1  5845  reseq2  5846  nfres  5853  csbres  5854  res0  5855  dfres3  5856  opelres  5857  resres  5864  resundi  5865  resundir  5866  resindi  5867  resindir  5868  inres  5869  resdifcom  5870  resiun1  5871  resiun2  5872  resss  5876  ssres  5878  ssres2  5879  relres  5880  xpssres  5888  elres  5890  resopab  5902  elrid  5913  imainrect  6044  xpima  6045  cnvcnv2  6056  cnvrescnv  6058  resdmres  6095  resdifdi  6099  resdifdir  6100  ressnop0  6968  fndifnfp  6991  tpres  7016  marypha1lem  9049  gsum2d  19357  gsumxp  19361  pjdm  20669  hausdiag  22542  isngp2  23495  ovoliunlem1  24399  xpdisjres  30656  difres  30658  imadifxp  30659  0res  30662  mbfmcst  31938  0rrv  32130  elrn3  33448  nosupbnd2lem1  33655  noetasuplem3  33675  noetasuplem4  33676  dfon4  33932  bj-opelresdm  35051  bj-idres  35066  bj-elid6  35076  restrreld  40952  csbresgVD  42188