Metamath Proof Explorer


Theorem fv2

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 ) }

Proof

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 ) }