This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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