df-doma - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-doma		Structured version Visualization version GIF version

Definition df-doma 17739

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

**Assertion**
Ref	Expression
df-doma	⊢ dom_a = (1^st ∘ 1^st )

**Detailed syntax breakdown of Definition df-doma**
Step	Hyp	Ref	Expression
1		cdoma 17735	. 2 class dom_a
2		c1st 7829	. . 3 class 1^st
3	2, 2	ccom 5593	. 2 class (1^st ∘ 1^st )
4	1, 3	wceq 1539	1 wff dom_a = (1^st ∘ 1^st )

Colors of variables: wff setvar class

This definition is referenced by: homadm 17755 dmaf 17764