Definition df-res 5666

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16136) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16081 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 30368). 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 6184). (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 5656	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3459	. . . 4 class V
5	2, 4	cxp 5652	. . 3 class (𝐵 × V)
6	1, 5	cin 3925	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1540	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5671  reseq1  5960  reseq2  5961  nfres  5968  csbres  5969  res0  5970  dfres3  5971  opelres  5972  resres  5979  resundi  5980  resundir  5981  resindi  5982  resindir  5983  inres  5984  resdifcom  5985  resiun1  5986  resiun2  5987  resss  5988  ssres  5990  ssres2  5991  relres  5992  xpssres  6005  elres  6007  resopab  6021  elrid  6033  imainrect  6170  xpima  6171  cnvcnv2  6182  cnvrescnv  6184  resdmres  6221  resdifdi  6225  resdifdir  6226  ressnop0  7142  fndifnfp  7167  tpres  7192  marypha1lem  9443  gsum2d  19951  gsumxp  19955  pjdm  21665  hausdiag  23581  isngp2  24534  ovoliunlem1  25453  nosupbnd2lem1  27677  noetasuplem3  27697  noetasuplem4  27698  xpdisjres  32525  difres  32527  imadifxp  32528  0res  32530  mbfmcst  34237  0rrv  34429  elrn3  35725  dfon4  35857  bj-opelresdm  37109  bj-idres  37124  bj-elid6  37134  br1cnvres  38233  restrreld  43638  csbresgVD  44867