Metamath Proof Explorer


Definition df-restrict

Description: Define the restriction function. See brrestrict for its value. (Contributed by Scott Fenton, 17-Apr-2014)

Ref Expression
Assertion df-restrict βŠ’π–±π–Ύπ—Œπ—π—‹π—‚π–Όπ—=π–’π–Ίπ—‰βˆ˜1stβŠ—π–’π–Ίπ—‹π—βˆ˜2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st

Detailed syntax breakdown

Step Hyp Ref Expression
0 crestrict classπ–±π–Ύπ—Œπ—π—‹π—‚π–Όπ—
1 ccap class𝖒𝖺𝗉
2 c1st class1st
3 ccart class𝖒𝖺𝗋𝗍
4 c2nd class2nd
5 crange class𝖱𝖺𝗇𝗀𝖾
6 5 2 ccom classπ–±π–Ίπ—‡π—€π–Ύβˆ˜1st
7 4 6 ctxp class2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st
8 3 7 ccom classπ–’π–Ίπ—‹π—βˆ˜2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st
9 2 8 ctxp class1stβŠ—π–’π–Ίπ—‹π—βˆ˜2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st
10 1 9 ccom classπ–’π–Ίπ—‰βˆ˜1stβŠ—π–’π–Ίπ—‹π—βˆ˜2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st
11 0 10 wceq wffπ–±π–Ύπ—Œπ—π—‹π—‚π–Όπ—=π–’π–Ίπ—‰βˆ˜1stβŠ—π–’π–Ίπ—‹π—βˆ˜2ndβŠ—π–±π–Ίπ—‡π—€π–Ύβˆ˜1st