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 5565
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15465) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15413 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 28134). 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 6049). (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 5555 . 2 class (𝐴𝐵)
4 cvv 3499 . . . 4 class V
52, 4cxp 5551 . . 3 class (𝐵 × V)
61, 5cin 3938 . 2 class (𝐴 ∩ (𝐵 × V))
73, 6wceq 1530 1 wff (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
Colors of variables: wff setvar class
This definition is referenced by:  inxpssres  5570  reseq1  5845  reseq2  5846  nfres  5853  csbres  5854  res0  5855  dfres3  5856  opelres  5857  resres  5864  resundi  5865  resundir  5866  resindi  5867  resindir  5868  inres  5869  resdifcom  5870  resiun1  5871  resiun2  5872  resss  5876  ssres  5878  ssres2  5879  relres  5880  xpssres  5887  elres  5889  resopab  5900  elrid  5911  imainrect  6035  xpima  6036  cnvcnv2  6047  cnvrescnv  6049  resdmres  6086  ressnop0  6910  fndifnfp  6933  tpres  6962  marypha1lem  8889  gsum2d  19014  gsumxp  19018  pjdm  20767  hausdiag  22169  isngp2  23121  ovoliunlem1  24018  xpdisjres  30263  difres  30265  imadifxp  30266  0res  30269  mbfmcst  31403  0rrv  31595  elrn3  32882  nosupbnd2lem1  33099  noetalem2  33102  noetalem3  33103  dfon4  33238  bj-opelresdm  34316  bj-idres  34331  bj-elid6  34341  restrreld  39873  csbresgVD  41090
  Copyright terms: Public domain W3C validator