Definition df-1st

Description: Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st proves that it does this. For example, ( 1st<. 3 , 4 >. ) = 3 . Equivalent to Definition 5.13 (i) of Monk1 p. 52 (compare op1sta and op1stb ). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004)

	Ref	Expression
Assertion	df-1st	$$⊢1^{st}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1st	$$class{1}^{st}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarx$$
4	3	csn	$$class\left\{x\right\}$$
5	4	cdm	$$class\mathrm{dom}\left\{x\right\}$$
6	5	cuni	$$class\bigcup \mathrm{dom}\left\{x\right\}$$
7	1 2 6	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$
8	0 7	wceq	$$wff{1}^{st}=\left(x\in \mathrm{V}⟼\bigcup \mathrm{dom}\left\{x\right\}\right)$$