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	⊢ dom_a = ( 1^st ∘ 1^st )

Step	Hyp	Ref	Expression
0		cdoma	⊢ dom_a
1		c1st	⊢ 1^st
2	1 1	ccom	⊢ ( 1^st ∘ 1^st )
3	0 2	wceq	⊢ dom_a = ( 1^st ∘ 1^st )