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