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

Metamath Proof Explorer

Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998) (Proof shortened by SN, 19-Dec-2024)

Ref Expression
Assertion funmo 
|- ( Fun F -> E* y A F y )

Proof

Step Hyp Ref Expression
1 dffun6 
 |-  ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )
2 1 simplbi 
 |-  ( Fun F -> Rel F )
3 brrelex1 
 |-  ( ( Rel F /\ A F y ) -> A e. _V )
4 3 ex 
 |-  ( Rel F -> ( A F y -> A e. _V ) )
5 2 4 syl 
 |-  ( Fun F -> ( A F y -> A e. _V ) )
6 5 ancrd 
 |-  ( Fun F -> ( A F y -> ( A e. _V /\ A F y ) ) )
7 6 alrimiv 
 |-  ( Fun F -> A. y ( A F y -> ( A e. _V /\ A F y ) ) )
8 1 simprbi 
 |-  ( Fun F -> A. x E* y x F y )
9 breq1 
 |-  ( x = A -> ( x F y <-> A F y ) )
10 9 mobidv 
 |-  ( x = A -> ( E* y x F y <-> E* y A F y ) )
11 10 spcgv 
 |-  ( A e. _V -> ( A. x E* y x F y -> E* y A F y ) )
12 8 11 syl5com 
 |-  ( Fun F -> ( A e. _V -> E* y A F y ) )
13 moanimv 
 |-  ( E* y ( A e. _V /\ A F y ) <-> ( A e. _V -> E* y A F y ) )
14 12 13 sylibr 
 |-  ( Fun F -> E* y ( A e. _V /\ A F y ) )
15 moim 
 |-  ( A. y ( A F y -> ( A e. _V /\ A F y ) ) -> ( E* y ( A e. _V /\ A F y ) -> E* y A F y ) )
16 7 14 15 sylc 
 |-  ( Fun F -> E* y A F y )