Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > df1st  Unicode version 
Description: Define a function that
extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6405 proves that it does this. For example,
?Error:
3 , 4 >. ) = 3
^
This math symbol is not active (i.e. was not declared in this scope).
( ` <. 3 , 4 >. ) = 3 . Equivalent to Definition 5.13 (i) of
[Monk1] p. 52 (compare op1sta 5397 and op1stb 4799). The notation is the same
as Monk's. (Contributed by NM, 9Oct2004.) 
Ref  Expression 

df1st 
Step  Hyp  Ref  Expression 

1  c1st 6397  . 2  
2  vx  . . 3  
3  cvv 2965  . . 3  
4  2  cv 1653  . . . . . 6 
5  4  csn 3841  . . . . 5 
6  5  cdm 4919  . . . 4 
7  6  cuni 4043  . . 3 
8  2, 3, 7  cmpt 4301  . 2 
9  1, 8  wceq 1654  1 
Colors of variables: wff set class 
This definition is referenced by: 1stval 6401 fo1st 6416 f1stres 6418 
Copyright terms: Public domain  W3C validator 