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

Metamath Proof Explorer

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} = (x \in V ⟼ ⋃ dom \{x\})$

Detailed syntax breakdown

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