Metamath Proof Explorer

Theorem fveu

Description: The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017)

Ref Expression
Assertion fveu 
|- ( E! x A F x -> ( F ` A ) = U. { x | A F x } )

Proof

Step Hyp Ref Expression
1 df-fv 
 |-  ( F ` A ) = ( iota x A F x )
2 iotauni 
 |-  ( E! x A F x -> ( iota x A F x ) = U. { x | A F x } )
3 1 2 eqtrid 
 |-  ( E! x A F x -> ( F ` A ) = U. { x | A F x } )