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 16060) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16008 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 29684). 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 6192). (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 3475	. . . 4 class V
5	2, 4	cxp 5674	. . 3 class (𝐵 × V)
6	1, 5	cin 3947	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1542	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5693  reseq1  5974  reseq2  5975  nfres  5982  csbres  5983  res0  5984  dfres3  5985  opelres  5986  resres  5993  resundi  5994  resundir  5995  resindi  5996  resindir  5997  inres  5998  resdifcom  5999  resiun1  6000  resiun2  6001  resss  6005  ssres  6007  ssres2  6008  relres  6009  xpssres  6017  elres  6019  resopab  6033  elrid  6044  imainrect  6178  xpima  6179  cnvcnv2  6190  cnvrescnv  6192  resdmres  6229  resdifdi  6233  resdifdir  6234  ressnop0  7148  fndifnfp  7171  tpres  7199  marypha1lem  9425  gsum2d  19835  gsumxp  19839  pjdm  21254  hausdiag  23141  isngp2  24098  ovoliunlem1  25011  nosupbnd2lem1  27208  noetasuplem3  27228  noetasuplem4  27229  xpdisjres  31817  difres  31819  imadifxp  31820  0res  31822  mbfmcst  33247  0rrv  33439  elrn3  34721  dfon4  34854  bj-opelresdm  36015  bj-idres  36030  bj-elid6  36040  br1cnvres  37126  restrreld  42404  csbresgVD  43642