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