Theorem funressnmo

Description: A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	funressnmo	|- ( ( A e. V /\ Fun ( F |` { A } ) ) -> E* y A F y )

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( x = A -> { x } = { A } )
2	1	reseq2d	|- ( x = A -> ( F |` { x } ) = ( F |` { A } ) )
3	2	funeqd	|- ( x = A -> ( Fun ( F |` { x } ) <-> Fun ( F |` { A } ) ) )
4		breq1	|- ( x = A -> ( x F y <-> A F y ) )
5	4	mobidv	|- ( x = A -> ( E* y x F y <-> E* y A F y ) )
6	3 5	imbi12d	|- ( x = A -> ( ( Fun ( F |` { x } ) -> E* y x F y ) <-> ( Fun ( F |` { A } ) -> E* y A F y ) ) )
7		funressnvmo	|- ( Fun ( F |` { x } ) -> E* y x F y )
8	6 7	vtoclg	|- ( A e. V -> ( Fun ( F |` { A } ) -> E* y A F y ) )
9	8	imp	|- ( ( A e. V /\ Fun ( F |` { A } ) ) -> E* y A F y )