Definition df-res 5653

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

This definition is referenced by:  inxpssres  5658  reseq1  5947  reseq2  5948  nfres  5955  csbres  5956  res0  5957  dfres3  5958  opelres  5959  resres  5966  resundi  5967  resundir  5968  resindi  5969  resindir  5970  inres  5971  resdifcom  5972  resiun1  5973  resiun2  5974  resss  5975  ssres  5977  ssres2  5978  relres  5979  xpssres  5992  elres  5994  resopab  6008  elrid  6020  imainrect  6157  xpima  6158  cnvcnv2  6169  cnvrescnv  6171  resdmres  6208  resdifdi  6212  resdifdir  6213  ressnop0  7128  fndifnfp  7153  tpres  7178  marypha1lem  9391  gsum2d  19909  gsumxp  19913  pjdm  21623  hausdiag  23539  isngp2  24492  ovoliunlem1  25410  nosupbnd2lem1  27634  noetasuplem3  27654  noetasuplem4  27655  xpdisjres  32534  difres  32536  imadifxp  32537  0res  32539  mbfmcst  34257  0rrv  34449  elrn3  35756  dfon4  35888  bj-opelresdm  37140  bj-idres  37155  bj-elid6  37165  br1cnvres  38265  restrreld  43663  csbresgVD  44891