Definition df-res 5667

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16314) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16259 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 31069). 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 6199). (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 5657	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3454	. . . 4 class V
5	2, 4	cxp 5653	. . 3 class (𝐵 × V)
6	1, 5	cin 4092	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1570	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  inxpssres  5672  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  6002  ssres  6004  ssres2  6005  relres  6006  relresOLD  6007  xpssres  6018  elres  6020  resopab  6037  elrid  6049  imainrect  6184  xpima  6185  cnvcnv2  6196  cnvrescnv  6199  resdmres  6245  resdifdi  6249  resdifdir  6250  ressnop0  7178  fndifnfp  7201  tpres  7227  marypha1lem  9449  gsum2d  20213  gsumxp  20217  pjdm  22040  hausdiag  23991  isngp2  24943  ovoliunlem1  25850  nosupbnd2lem1  28099  noetasuplem3  28119  noetasuplem4  28120  xpdisjres  33261  difres  33263  imadifxp  33264  0res  33266  mbfmcst  34958  0rrv  35150  elrn3  36704  dfon4  36832  bj-elres  38139  bj-resss2  38141  bj-dfrel3  38143  bj-cnvcnv  38148  bj-opelresdm  38257  bj-idres  38272  bj-elid6  38282  br1cnvres  39397  restrreld  44857  csbresgVD  46066