This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )