Step |
Hyp |
Ref |
Expression |
1 |
|
funrel |
|- ( Fun F -> Rel F ) |
2 |
|
releldm |
|- ( ( Rel F /\ A F B ) -> A e. dom F ) |
3 |
2
|
ex |
|- ( Rel F -> ( A F B -> A e. dom F ) ) |
4 |
1 3
|
syl |
|- ( Fun F -> ( A F B -> A e. dom F ) ) |
5 |
4
|
pm4.71rd |
|- ( Fun F -> ( A F B <-> ( A e. dom F /\ A F B ) ) ) |
6 |
|
funbrfvb |
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) = B <-> A F B ) ) |
7 |
6
|
pm5.32da |
|- ( Fun F -> ( ( A e. dom F /\ ( F ` A ) = B ) <-> ( A e. dom F /\ A F B ) ) ) |
8 |
5 7
|
bitr4d |
|- ( Fun F -> ( A F B <-> ( A e. dom F /\ ( F ` A ) = B ) ) ) |