Definition df-res 5688

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16067) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16015 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 29949). 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 6194). (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 5678	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3474	. . . 4 class V
5	2, 4	cxp 5674	. . 3 class (𝐵 × V)
6	1, 5	cin 3947	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1541	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5693  reseq1  5975  reseq2  5976  nfres  5983  csbres  5984  res0  5985  dfres3  5986  opelres  5987  resres  5994  resundi  5995  resundir  5996  resindi  5997  resindir  5998  inres  5999  resdifcom  6000  resiun1  6001  resiun2  6002  resss  6006  ssres  6008  ssres2  6009  relres  6010  xpssres  6018  elres  6020  resopab  6034  elrid  6045  imainrect  6180  xpima  6181  cnvcnv2  6192  cnvrescnv  6194  resdmres  6231  resdifdi  6235  resdifdir  6236  ressnop0  7153  fndifnfp  7176  tpres  7204  marypha1lem  9430  gsum2d  19881  gsumxp  19885  pjdm  21481  hausdiag  23369  isngp2  24326  ovoliunlem1  25243  nosupbnd2lem1  27442  noetasuplem3  27462  noetasuplem4  27463  xpdisjres  32084  difres  32086  imadifxp  32087  0res  32089  mbfmcst  33544  0rrv  33736  elrn3  35024  dfon4  35157  bj-opelresdm  36329  bj-idres  36344  bj-elid6  36354  br1cnvres  37440  restrreld  42720  csbresgVD  43958