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 1st = ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1st ⊢ 1st
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 1 cv ⊢ 𝑥
4 3 csn ⊢ { 𝑥 }
5 4 cdm ⊢ dom { 𝑥 }
6 5 cuni ⊢ ∪ dom { 𝑥 }
7 1 2 6 cmpt ⊢ ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )
8 0 7 wceq ⊢ 1st = ( 𝑥 ∈ V ↦ ∪ dom { 𝑥 } )