Metamath Proof Explorer


Theorem dffv4

Description: The previous definition of function value, from before the iota operator was introduced. Although based on the idea embodied by Definition 10.2 of Quine p. 65 (see args ), this definition apparently does not appear in the literature. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion dffv4
|- ( F ` A ) = U. { x | ( F " { A } ) = { x } }

Proof

Step Hyp Ref Expression
1 dffv3
 |-  ( F ` A ) = ( iota y y e. ( F " { A } ) )
2 df-iota
 |-  ( iota y y e. ( F " { A } ) ) = U. { x | { y | y e. ( F " { A } ) } = { x } }
3 abid2
 |-  { y | y e. ( F " { A } ) } = ( F " { A } )
4 3 eqeq1i
 |-  ( { y | y e. ( F " { A } ) } = { x } <-> ( F " { A } ) = { x } )
5 4 abbii
 |-  { x | { y | y e. ( F " { A } ) } = { x } } = { x | ( F " { A } ) = { x } }
6 5 unieqi
 |-  U. { x | { y | y e. ( F " { A } ) } = { x } } = U. { x | ( F " { A } ) = { x } }
7 1 2 6 3eqtri
 |-  ( F ` A ) = U. { x | ( F " { A } ) = { x } }