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}\circ 1^{st}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdoma	$$class{dom}_a$$
1		c1st	$$class{1}^{st}$$
2	1 1	ccom	$$class\left(1^{st}\circ 1^{st}\right)$$
3	0 2	wceq	$$wff{dom}_a=1^{st}\circ 1^{st}$$