Definition df-res 5050

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 14689) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 14637 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩} (ex-res 26690). (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 5040	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3173	. . . 4 class V
5	2, 4	cxp 5036	. . 3 class (𝐵 × V)
6	1, 5	cin 3539	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1475	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  5311  reseq2  5312  nfres  5319  csbres  5320  res0  5321  opelres  5322  resres  5329  resundi  5330  resundir  5331  resindi  5332  resindir  5333  inres  5334  resdifcom  5335  resiun1  5336  resiun1OLD  5337  resiun2  5338  resss  5342  ssres  5344  ssres2  5345  relres  5346  xpssres  5354  resopab  5366  ssrnres  5491  imainrect  5494  xpima  5495  cnvcnv2  5506  resdmres  5543  ressnop0  6325  fndifnfp  6347  tpres  6371  marypha1lem  8222  gsum2d  18194  gsumxp  18198  pjdm  19870  hausdiag  21258  isngp2  22211  ovoliunlem1  23077  xpdisjres  28793  difres  28795  imadifxp  28796  mbfmcst  29648  0rrv  29840  dfres3  30902  elrn3  30906  dfon4  31170  restrreld  36978  csbresgOLD  38077  csbresgVD  38153