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 15473) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15421 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 28220). 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 6052). (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 5557 | . 2 class (𝐴 ↾ 𝐵) |
4 | cvv 3494 | . . . 4 class V | |
5 | 2, 4 | cxp 5553 | . . 3 class (𝐵 × V) |
6 | 1, 5 | cin 3935 | . 2 class (𝐴 ∩ (𝐵 × V)) |
7 | 3, 6 | wceq 1537 | 1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
Colors of variables: wff setvar class |
This definition is referenced by: inxpssres 5572 reseq1 5847 reseq2 5848 nfres 5855 csbres 5856 res0 5857 dfres3 5858 opelres 5859 resres 5866 resundi 5867 resundir 5868 resindi 5869 resindir 5870 inres 5871 resdifcom 5872 resiun1 5873 resiun2 5874 resss 5878 ssres 5880 ssres2 5881 relres 5882 xpssres 5889 elres 5891 resopab 5902 elrid 5913 imainrect 6038 xpima 6039 cnvcnv2 6050 cnvrescnv 6052 resdmres 6089 ressnop0 6915 fndifnfp 6938 tpres 6963 marypha1lem 8897 gsum2d 19092 gsumxp 19096 pjdm 20851 hausdiag 22253 isngp2 23206 ovoliunlem1 24103 xpdisjres 30348 difres 30350 imadifxp 30351 0res 30354 mbfmcst 31517 0rrv 31709 elrn3 32998 nosupbnd2lem1 33215 noetalem2 33218 noetalem3 33219 dfon4 33354 bj-opelresdm 34440 bj-idres 34455 bj-elid6 34465 restrreld 40061 csbresgVD 41278 |
Copyright terms: Public domain | W3C validator |