Step |
Hyp |
Ref |
Expression |
1 |
|
eqcom |
|- ( y = ( F '''' A ) <-> ( F '''' A ) = y ) |
2 |
|
dfatbrafv2b |
|- ( ( F defAt A /\ y e. _V ) -> ( ( F '''' A ) = y <-> A F y ) ) |
3 |
2
|
elvd |
|- ( F defAt A -> ( ( F '''' A ) = y <-> A F y ) ) |
4 |
1 3
|
syl5bb |
|- ( F defAt A -> ( y = ( F '''' A ) <-> A F y ) ) |
5 |
4
|
abbidv |
|- ( F defAt A -> { y | y = ( F '''' A ) } = { y | A F y } ) |
6 |
|
df-sn |
|- { ( F '''' A ) } = { y | y = ( F '''' A ) } |
7 |
6
|
a1i |
|- ( F defAt A -> { ( F '''' A ) } = { y | y = ( F '''' A ) } ) |
8 |
|
dfdfat2 |
|- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) ) |
9 |
|
imasng |
|- ( A e. dom F -> ( F " { A } ) = { y | A F y } ) |
10 |
9
|
adantr |
|- ( ( A e. dom F /\ E! x A F x ) -> ( F " { A } ) = { y | A F y } ) |
11 |
8 10
|
sylbi |
|- ( F defAt A -> ( F " { A } ) = { y | A F y } ) |
12 |
5 7 11
|
3eqtr4d |
|- ( F defAt A -> { ( F '''' A ) } = ( F " { A } ) ) |