Definition df-res 5661

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16154) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16099 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 30645). 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 5651	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3456	. . . 4 class V
5	2, 4	cxp 5647	. . 3 class (𝐵 × V)
6	1, 5	cin 3905	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1562	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5666  reseq1  5961  reseq2  5962  nfres  5969  csbres  5970  res0  5971  dfres3  5972  opelres  5973  resres  5980  resundi  5981  resundir  5982  resindi  5983  resindir  5984  inres  5985  resdifcom  5986  resiun1  5987  resiun2  5988  resss  5989  ssres  5991  ssres2  5992  relres  5993  xpssres  6006  elres  6008  resopab  6025  elrid  6037  imainrect  6169  xpima  6170  cnvcnv2  6181  cnvrescnv  6184  resdmres  6221  resdifdi  6225  resdifdir  6226  ressnop0  7138  fndifnfp  7162  tpres  7187  marypha1lem  9381  gsum2d  20014  gsumxp  20018  pjdm  21761  hausdiag  23707  isngp2  24659  ovoliunlem1  25566  nosupbnd2lem1  27781  noetasuplem3  27801  noetasuplem4  27802  xpdisjres  32800  difres  32802  imadifxp  32803  0res  32805  mbfmcst  34558  0rrv  34750  elrn3  36117  dfon4  36246  bj-opelresdm  37642  bj-idres  37657  bj-elid6  37667  br1cnvres  38778  restrreld  44248  csbresgVD  45475