Definition df-res 5672

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16182) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16127 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 30803). 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 6193). (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 5662	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3454	. . . 4 class V
5	2, 4	cxp 5658	. . 3 class (𝐵 × V)
6	1, 5	cin 3903	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1569	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  inxpssres  5677  reseq1  5971  reseq2  5972  nfres  5979  csbres  5980  res0  5981  dfres3  5982  opelres  5983  resres  5990  resundi  5991  resundir  5992  resindi  5993  resindir  5994  inres  5995  resdifcom  5996  resiun1  5997  resiun2  5998  resss  5999  ssres  6001  ssres2  6002  relres  6003  xpssres  6016  elres  6018  resopab  6035  elrid  6047  imainrect  6178  xpima  6179  cnvcnv2  6190  cnvrescnv  6193  resdmres  6232  resdifdi  6236  resdifdir  6237  ressnop0  7150  fndifnfp  7174  tpres  7199  marypha1lem  9391  gsum2d  20048  gsumxp  20052  pjdm  21868  hausdiag  23813  isngp2  24765  ovoliunlem1  25672  nosupbnd2lem1  27890  noetasuplem3  27910  noetasuplem4  27911  xpdisjres  32954  difres  32956  imadifxp  32957  0res  32959  mbfmcst  34658  0rrv  34850  elrn3  36262  dfon4  36391  bj-opelresdm  37817  bj-idres  37832  bj-elid6  37842  br1cnvres  38951  restrreld  44421  csbresgVD  45631