Metamath Proof Explorer

Definition df-domain

Description: Define the domain function. See brdomain for its value. (Contributed by Scott Fenton, 11-Apr-2014)

Ref Expression
Assertion df-domain 
|- Domain = Image ( 1st |` ( _V X. _V ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdomain 
 |-  Domain
1 c1st 
 |-  1st
2 cvv 
 |-  _V
3 2 2 cxp 
 |-  ( _V X. _V )
4 1 3 cres 
 |-  ( 1st |` ( _V X. _V ) )
5 4 cimage 
 |-  Image ( 1st |` ( _V X. _V ) )
6 0 5 wceq 
 |-  Domain = Image ( 1st |` ( _V X. _V ) )