Definition df-res 5712

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16168) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16115 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 30473). 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 6226). (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 5702	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3488	. . . 4 class V
5	2, 4	cxp 5698	. . 3 class (𝐵 × V)
6	1, 5	cin 3975	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1537	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5717  reseq1  6003  reseq2  6004  nfres  6011  csbres  6012  res0  6013  dfres3  6014  opelres  6015  resres  6022  resundi  6023  resundir  6024  resindi  6025  resindir  6026  inres  6027  resdifcom  6028  resiun1  6029  resiun2  6030  resss  6031  ssres  6033  ssres2  6034  relres  6035  xpssres  6047  elres  6049  resopab  6063  elrid  6075  imainrect  6212  xpima  6213  cnvcnv2  6224  cnvrescnv  6226  resdmres  6263  resdifdi  6267  resdifdir  6268  ressnop0  7187  fndifnfp  7210  tpres  7238  marypha1lem  9502  gsum2d  20014  gsumxp  20018  pjdm  21750  hausdiag  23674  isngp2  24631  ovoliunlem1  25556  nosupbnd2lem1  27778  noetasuplem3  27798  noetasuplem4  27799  xpdisjres  32620  difres  32622  imadifxp  32623  0res  32625  mbfmcst  34224  0rrv  34416  elrn3  35724  dfon4  35857  bj-opelresdm  37111  bj-idres  37126  bj-elid6  37136  br1cnvres  38225  restrreld  43629  csbresgVD  44866