Metamath Proof Explorer


Definition df-img

Description: Define the image function. See brimg for its value. (Contributed by Scott Fenton, 12-Apr-2014)

Ref Expression
Assertion df-img 𝖨𝗆𝗀 = 𝖨𝗆𝖺𝗀𝖾 2 nd 1 st 1 st V × V 𝖢𝖺𝗋𝗍

Detailed syntax breakdown

Step Hyp Ref Expression
0 cimg class 𝖨𝗆𝗀
1 c2nd class 2 nd
2 c1st class 1 st
3 1 2 ccom class 2 nd 1 st
4 cvv class V
5 4 4 cxp class V × V
6 2 5 cres class 1 st V × V
7 3 6 cres class 2 nd 1 st 1 st V × V
8 7 cimage class 𝖨𝗆𝖺𝗀𝖾 2 nd 1 st 1 st V × V
9 ccart class 𝖢𝖺𝗋𝗍
10 8 9 ccom class 𝖨𝗆𝖺𝗀𝖾 2 nd 1 st 1 st V × V 𝖢𝖺𝗋𝗍
11 0 10 wceq wff 𝖨𝗆𝗀 = 𝖨𝗆𝖺𝗀𝖾 2 nd 1 st 1 st V × V 𝖢𝖺𝗋𝗍