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

Metamath Proof Explorer

Theorem fvfundmfvn0

Description: If the "value of a class" at an argument is not the empty set, then the argument is in the domain of the class and the class restricted to the singleton formed on that argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017) (Proof shortened by BJ, 13-Aug-2022)

Ref Expression
Assertion fvfundmfvn0 
|- ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )

Proof

Step Hyp Ref Expression
1 ndmfv 
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
2 1 necon1ai 
 |-  ( ( F ` A ) =/= (/) -> A e. dom F )
3 nfunsn 
 |-  ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )
4 3 necon1ai 
 |-  ( ( F ` A ) =/= (/) -> Fun ( F |` { A } ) )
5 2 4 jca 
 |-  ( ( F ` A ) =/= (/) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )