Definition df-res 5637

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16049) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15994 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 30520). 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 6154). (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 5627	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3441	. . . 4 class V
5	2, 4	cxp 5623	. . 3 class (𝐵 × V)
6	1, 5	cin 3901	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1542	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5642  reseq1  5933  reseq2  5934  nfres  5941  csbres  5942  res0  5943  dfres3  5944  opelres  5945  resres  5952  resundi  5953  resundir  5954  resindi  5955  resindir  5956  inres  5957  resdifcom  5958  resiun1  5959  resiun2  5960  resss  5961  ssres  5963  ssres2  5964  relres  5965  xpssres  5978  elres  5980  resopab  5994  elrid  6006  imainrect  6140  xpima  6141  cnvcnv2  6152  cnvrescnv  6154  resdmres  6191  resdifdi  6195  resdifdir  6196  ressnop0  7100  fndifnfp  7124  tpres  7149  marypha1lem  9340  gsum2d  19905  gsumxp  19909  pjdm  21666  hausdiag  23593  isngp2  24545  ovoliunlem1  25463  nosupbnd2lem1  27687  noetasuplem3  27707  noetasuplem4  27708  xpdisjres  32676  difres  32678  imadifxp  32679  0res  32681  mbfmcst  34418  0rrv  34610  elrn3  35958  dfon4  36087  bj-opelresdm  37352  bj-idres  37367  bj-elid6  37377  br1cnvres  38477  restrreld  43975  csbresgVD  45202