| 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 16156) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16103 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 30460). 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 6215). (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 5687 | . 2 class (𝐴 ↾ 𝐵) |
| 4 | cvv 3480 | . . . 4 class V | |
| 5 | 2, 4 | cxp 5683 | . . 3 class (𝐵 × V) |
| 6 | 1, 5 | cin 3950 | . 2 class (𝐴 ∩ (𝐵 × V)) |
| 7 | 3, 6 | wceq 1540 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: inxpssres 5702 reseq1 5991 reseq2 5992 nfres 5999 csbres 6000 res0 6001 dfres3 6002 opelres 6003 resres 6010 resundi 6011 resundir 6012 resindi 6013 resindir 6014 inres 6015 resdifcom 6016 resiun1 6017 resiun2 6018 resss 6019 ssres 6021 ssres2 6022 relres 6023 xpssres 6036 elres 6038 resopab 6052 elrid 6064 imainrect 6201 xpima 6202 cnvcnv2 6213 cnvrescnv 6215 resdmres 6252 resdifdi 6256 resdifdir 6257 ressnop0 7173 fndifnfp 7196 tpres 7221 marypha1lem 9473 gsum2d 19990 gsumxp 19994 pjdm 21727 hausdiag 23653 isngp2 24610 ovoliunlem1 25537 nosupbnd2lem1 27760 noetasuplem3 27780 noetasuplem4 27781 xpdisjres 32611 difres 32613 imadifxp 32614 0res 32616 mbfmcst 34261 0rrv 34453 elrn3 35762 dfon4 35894 bj-opelresdm 37146 bj-idres 37161 bj-elid6 37171 br1cnvres 38270 restrreld 43680 csbresgVD 44915 |
| Copyright terms: Public domain | W3C validator |