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 15681) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15629 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 28524). 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 6058). (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 5553 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 3408 | . . . 4 class V | |
5 | 2, 4 | cxp 5549 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3865 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 1543 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: inxpssres 5568 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 5888 elres 5890 resopab 5902 elrid 5913 imainrect 6044 xpima 6045 cnvcnv2 6056 cnvrescnv 6058 resdmres 6095 resdifdi 6099 resdifdir 6100 ressnop0 6968 fndifnfp 6991 tpres 7016 marypha1lem 9049 gsum2d 19357 gsumxp 19361 pjdm 20669 hausdiag 22542 isngp2 23495 ovoliunlem1 24399 xpdisjres 30656 difres 30658 imadifxp 30659 0res 30662 mbfmcst 31938 0rrv 32130 elrn3 33448 nosupbnd2lem1 33655 noetasuplem3 33675 noetasuplem4 33676 dfon4 33932 bj-opelresdm 35051 bj-idres 35066 bj-elid6 35076 restrreld 40952 csbresgVD 42188 |
Copyright terms: Public domain | W3C validator |