Definition df-res 5697

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

This definition is referenced by:  inxpssres  5702  reseq1  5991  reseq2  5992  nfres  5999  csbres  6000  res0  6001  dfres3  6002  opelres  6003  resres  6010  resundi  6011  resundir  6012  resindi  6013  resindir  6014  inres  6015  resdifcom  6016  resiun1  6017  resiun2  6018  resss  6019  ssres  6021  ssres2  6022  relres  6023  xpssres  6036  elres  6038  resopab  6052  elrid  6064  imainrect  6201  xpima  6202  cnvcnv2  6213  cnvrescnv  6215  resdmres  6252  resdifdi  6256  resdifdir  6257  ressnop0  7173  fndifnfp  7196  tpres  7221  marypha1lem  9473  gsum2d  19990  gsumxp  19994  pjdm  21727  hausdiag  23653  isngp2  24610  ovoliunlem1  25537  nosupbnd2lem1  27760  noetasuplem3  27780  noetasuplem4  27781  xpdisjres  32611  difres  32613  imadifxp  32614  0res  32616  mbfmcst  34261  0rrv  34453  elrn3  35762  dfon4  35894  bj-opelresdm  37146  bj-idres  37161  bj-elid6  37171  br1cnvres  38270  restrreld  43680  csbresgVD  44915