| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imasng |
|- ( B e. A -> ( F " { B } ) = { y | B F y } ) |
| 2 |
1
|
adantl |
|- ( ( F Fn A /\ B e. A ) -> ( F " { B } ) = { y | B F y } ) |
| 3 |
|
velsn |
|- ( y e. { ( F ` B ) } <-> y = ( F ` B ) ) |
| 4 |
|
eqcom |
|- ( y = ( F ` B ) <-> ( F ` B ) = y ) |
| 5 |
3 4
|
bitri |
|- ( y e. { ( F ` B ) } <-> ( F ` B ) = y ) |
| 6 |
|
fnbrfvb |
|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = y <-> B F y ) ) |
| 7 |
5 6
|
bitr2id |
|- ( ( F Fn A /\ B e. A ) -> ( B F y <-> y e. { ( F ` B ) } ) ) |
| 8 |
7
|
eqabcdv |
|- ( ( F Fn A /\ B e. A ) -> { y | B F y } = { ( F ` B ) } ) |
| 9 |
2 8
|
eqtr2d |
|- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) ) |