Description: Alternate definition of function value. Definition 10.11 of Quine p. 68. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Revised by Mario Carneiro, 31-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fv2 | |- ( F ` A ) = U. { x | A. y ( A F y <-> y = x ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fv | |- ( F ` A ) = ( iota y A F y ) |
|
2 | dfiota2 | |- ( iota y A F y ) = U. { x | A. y ( A F y <-> y = x ) } |
|
3 | 1 2 | eqtri | |- ( F ` A ) = U. { x | A. y ( A F y <-> y = x ) } |