Definition df-res 5567

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15473) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15421 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩} (ex-res 28220). 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 6052). (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 5557	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3494	. . . 4 class V
5	2, 4	cxp 5553	. . 3 class (𝐵 × V)
6	1, 5	cin 3935	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1537	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5572  reseq1  5847  reseq2  5848  nfres  5855  csbres  5856  res0  5857  dfres3  5858  opelres  5859  resres  5866  resundi  5867  resundir  5868  resindi  5869  resindir  5870  inres  5871  resdifcom  5872  resiun1  5873  resiun2  5874  resss  5878  ssres  5880  ssres2  5881  relres  5882  xpssres  5889  elres  5891  resopab  5902  elrid  5913  imainrect  6038  xpima  6039  cnvcnv2  6050  cnvrescnv  6052  resdmres  6089  ressnop0  6915  fndifnfp  6938  tpres  6963  marypha1lem  8897  gsum2d  19092  gsumxp  19096  pjdm  20851  hausdiag  22253  isngp2  23206  ovoliunlem1  24103  xpdisjres  30348  difres  30350  imadifxp  30351  0res  30354  mbfmcst  31517  0rrv  31709  elrn3  32998  nosupbnd2lem1  33215  noetalem2  33218  noetalem3  33219  dfon4  33354  bj-opelresdm  34440  bj-idres  34455  bj-elid6  34465  restrreld  40061  csbresgVD  41278