This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem feu

Description: There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003)

Ref Expression
Assertion feu 
|- ( ( F : A --> B /\ C e. A ) -> E! y e. B <. C , y >. e. F )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 fneu2 
 |-  ( ( F Fn A /\ C e. A ) -> E! y <. C , y >. e. F )
3 1 2 sylan 
 |-  ( ( F : A --> B /\ C e. A ) -> E! y <. C , y >. e. F )
4 opelf 
 |-  ( ( F : A --> B /\ <. C , y >. e. F ) -> ( C e. A /\ y e. B ) )
5 4 simprd 
 |-  ( ( F : A --> B /\ <. C , y >. e. F ) -> y e. B )
6 5 ex 
 |-  ( F : A --> B -> ( <. C , y >. e. F -> y e. B ) )
7 6 pm4.71rd 
 |-  ( F : A --> B -> ( <. C , y >. e. F <-> ( y e. B /\ <. C , y >. e. F ) ) )
8 7 eubidv 
 |-  ( F : A --> B -> ( E! y <. C , y >. e. F <-> E! y ( y e. B /\ <. C , y >. e. F ) ) )
9 8 adantr 
 |-  ( ( F : A --> B /\ C e. A ) -> ( E! y <. C , y >. e. F <-> E! y ( y e. B /\ <. C , y >. e. F ) ) )
10 3 9 mpbid 
 |-  ( ( F : A --> B /\ C e. A ) -> E! y ( y e. B /\ <. C , y >. e. F ) )
11 df-reu 
 |-  ( E! y e. B <. C , y >. e. F <-> E! y ( y e. B /\ <. C , y >. e. F ) )
12 10 11 sylibr 
 |-  ( ( F : A --> B /\ C e. A ) -> E! y e. B <. C , y >. e. F )