MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-res Structured version   Visualization version   GIF version

Definition df-res 5561
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15463) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15411 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 28148). 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 6046). (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-res (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cres 5551 . 2 class (𝐴𝐵)
4 cvv 3495 . . . 4 class V
52, 4cxp 5547 . . 3 class (𝐵 × V)
61, 5cin 3934 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1528 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  inxpssres  5566  reseq1  5841  reseq2  5842  nfres  5849  csbres  5850  res0  5851  dfres3  5852  opelres  5853  resres  5860  resundi  5861  resundir  5862  resindi  5863  resindir  5864  inres  5865  resdifcom  5866  resiun1  5867  resiun2  5868  resss  5872  ssres  5874  ssres2  5875  relres  5876  xpssres  5883  elres  5885  resopab  5896  elrid  5907  imainrect  6032  xpima  6033  cnvcnv2  6044  cnvrescnv  6046  resdmres  6083  ressnop0  6908  fndifnfp  6931  tpres  6956  marypha1lem  8886  gsum2d  19023  gsumxp  19027  pjdm  20781  hausdiag  22183  isngp2  23135  ovoliunlem1  24032  xpdisjres  30277  difres  30279  imadifxp  30280  0res  30283  mbfmcst  31417  0rrv  31609  elrn3  32896  nosupbnd2lem1  33113  noetalem2  33116  noetalem3  33117  dfon4  33252  bj-opelresdm  34330  bj-idres  34345  bj-elid6  34355  restrreld  39892  csbresgVD  41109
  Copyright terms: Public domain W3C validator