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	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
2	1	necon1ai	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐴 ∈ dom 𝐹 )
3		nfunsn	⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
4	3	necon1ai	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → Fun ( 𝐹 ↾ { 𝐴 } ) )
5	2 4	jca	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )