Description: Example for df-1st . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ex-1st | |- ( 1st ` <. 3 , 4 >. ) = 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ex | |- 3 e. _V |
|
2 | 4re | |- 4 e. RR |
|
3 | 2 | elexi | |- 4 e. _V |
4 | 1 3 | op1st | |- ( 1st ` <. 3 , 4 >. ) = 3 |