Metamath Proof Explorer

Definition df-doma

Description: Definition of the domain extractor for an arrow. (Contributed by FL, 24-Oct-2007) (Revised by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-doma 
|- domA = ( 1st o. 1st )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdoma 
 |-  domA
1 c1st 
 |-  1st
2 1 1 ccom 
 |-  ( 1st o. 1st )
3 0 2 wceq 
 |-  domA = ( 1st o. 1st )