Definition df-res 5600

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15836) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15784 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 28812). 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 6101). (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 5590	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3431	. . . 4 class V
5	2, 4	cxp 5586	. . 3 class (𝐵 × V)
6	1, 5	cin 3885	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1538	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5605  reseq1  5886  reseq2  5887  nfres  5894  csbres  5895  res0  5896  dfres3  5897  opelres  5898  resres  5905  resundi  5906  resundir  5907  resindi  5908  resindir  5909  inres  5910  resdifcom  5911  resiun1  5912  resiun2  5913  resss  5917  ssres  5919  ssres2  5920  relres  5921  xpssres  5929  elres  5931  resopab  5943  elrid  5954  imainrect  6087  xpima  6088  cnvcnv2  6099  cnvrescnv  6101  resdmres  6138  resdifdi  6142  resdifdir  6143  ressnop0  7032  fndifnfp  7055  tpres  7083  marypha1lem  9199  gsum2d  19580  gsumxp  19584  pjdm  20921  hausdiag  22803  isngp2  23760  ovoliunlem1  24673  xpdisjres  30944  difres  30946  imadifxp  30947  0res  30950  mbfmcst  32233  0rrv  32425  elrn3  33736  nosupbnd2lem1  33925  noetasuplem3  33945  noetasuplem4  33946  dfon4  34202  bj-opelresdm  35323  bj-idres  35338  bj-elid6  35348  restrreld  41280  csbresgVD  42520