Definition df-res 5640

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

This definition is referenced by:  inxpssres  5645  reseq1  5936  reseq2  5937  nfres  5944  csbres  5945  res0  5946  dfres3  5947  opelres  5948  resres  5955  resundi  5956  resundir  5957  resindi  5958  resindir  5959  inres  5960  resdifcom  5961  resiun1  5962  resiun2  5963  resss  5964  ssres  5966  ssres2  5967  relres  5968  xpssres  5981  elres  5983  resopab  5997  elrid  6009  imainrect  6143  xpima  6144  cnvcnv2  6155  cnvrescnv  6157  resdmres  6194  resdifdi  6198  resdifdir  6199  ressnop0  7104  fndifnfp  7128  tpres  7153  marypha1lem  9343  gsum2d  19944  gsumxp  19948  pjdm  21684  hausdiag  23607  isngp2  24559  ovoliunlem1  25466  nosupbnd2lem1  27676  noetasuplem3  27696  noetasuplem4  27697  xpdisjres  32665  difres  32667  imadifxp  32668  0res  32670  mbfmcst  34400  0rrv  34592  elrn3  35941  dfon4  36070  bj-opelresdm  37456  bj-idres  37471  bj-elid6  37481  br1cnvres  38592  restrreld  44091  csbresgVD  45318