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

Definition df-res 5531
 Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15467) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15415 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 28233). 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 6019). (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 5521 . 2 class (𝐴𝐵)
4 cvv 3441 . . . 4 class V
52, 4cxp 5517 . . 3 class (𝐵 × V)
61, 5cin 3880 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1538 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
 Colors of variables: wff setvar class This definition is referenced by:  inxpssres  5536  reseq1  5812  reseq2  5813  nfres  5820  csbres  5821  res0  5822  dfres3  5823  opelres  5824  resres  5831  resundi  5832  resundir  5833  resindi  5834  resindir  5835  inres  5836  resdifcom  5837  resiun1  5838  resiun2  5839  resss  5843  ssres  5845  ssres2  5846  relres  5847  xpssres  5855  elres  5857  resopab  5869  elrid  5880  imainrect  6005  xpima  6006  cnvcnv2  6017  cnvrescnv  6019  resdmres  6056  ressnop0  6892  fndifnfp  6915  tpres  6940  marypha1lem  8883  gsum2d  19088  gsumxp  19092  pjdm  20400  hausdiag  22257  isngp2  23210  ovoliunlem1  24113  xpdisjres  30368  difres  30370  imadifxp  30371  0res  30374  mbfmcst  31639  0rrv  31831  elrn3  33123  nosupbnd2lem1  33340  noetalem2  33343  noetalem3  33344  dfon4  33479  bj-opelresdm  34576  bj-idres  34591  bj-elid6  34601  restrreld  40383  csbresgVD  41616
 Copyright terms: Public domain W3C validator