Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-res | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-res | ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cres 5551 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 3495 | . . . 4 class V | |
5 | 2, 4 | cxp 5547 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3934 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 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 |