Step |
Hyp |
Ref |
Expression |
1 |
|
feu |
|- ( ( F : A --> B /\ X e. A ) -> E! y e. B <. X , y >. e. F ) |
2 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
3 |
2
|
anim1i |
|- ( ( F : A --> B /\ X e. A ) -> ( F Fn A /\ X e. A ) ) |
4 |
3
|
adantr |
|- ( ( ( F : A --> B /\ X e. A ) /\ y e. B ) -> ( F Fn A /\ X e. A ) ) |
5 |
|
fnopfvb |
|- ( ( F Fn A /\ X e. A ) -> ( ( F ` X ) = y <-> <. X , y >. e. F ) ) |
6 |
4 5
|
syl |
|- ( ( ( F : A --> B /\ X e. A ) /\ y e. B ) -> ( ( F ` X ) = y <-> <. X , y >. e. F ) ) |
7 |
6
|
reubidva |
|- ( ( F : A --> B /\ X e. A ) -> ( E! y e. B ( F ` X ) = y <-> E! y e. B <. X , y >. e. F ) ) |
8 |
1 7
|
mpbird |
|- ( ( F : A --> B /\ X e. A ) -> E! y e. B ( F ` X ) = y ) |