Theorem dffv5

Description: Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	dffv5	|- ( F ` A ) = U. U. ( { ( F " { A } ) } i^i Singletons )

Proof

Step	Hyp	Ref	Expression
1		dffv3	|- ( F ` A ) = ( iota x x e. ( F " { A } ) )
2		dfiota3	|- ( iota x x e. ( F " { A } ) ) = U. U. ( { { x | x e. ( F " { A } ) } } i^i Singletons )
3		abid2	|- { x | x e. ( F " { A } ) } = ( F " { A } )
4	3	sneqi	|- { { x | x e. ( F " { A } ) } } = { ( F " { A } ) }
5	4	ineq1i	|- ( { { x | x e. ( F " { A } ) } } i^i Singletons ) = ( { ( F " { A } ) } i^i Singletons )
6	5	unieqi	|- U. ( { { x | x e. ( F " { A } ) } } i^i Singletons ) = U. ( { ( F " { A } ) } i^i Singletons )
7	6	unieqi	|- U. U. ( { { x | x e. ( F " { A } ) } } i^i Singletons ) = U. U. ( { ( F " { A } ) } i^i Singletons )
8	1 2 7	3eqtri	|- ( F ` A ) = U. U. ( { ( F " { A } ) } i^i Singletons )