Theorem funressnvmo

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	funressnvmo	|- ( Fun ( F |` { x } ) -> E* y x F y )

Proof

Step	Hyp	Ref	Expression
1		dffun6	|- ( Fun ( F |` { x } ) <-> ( Rel ( F |` { x } ) /\ A. z E* y z ( F |` { x } ) y ) )
2		breq1	|- ( x = z -> ( x ( F |` { x } ) y <-> z ( F |` { x } ) y ) )
3	2	equcoms	|- ( z = x -> ( x ( F |` { x } ) y <-> z ( F |` { x } ) y ) )
4	3	biimpd	|- ( z = x -> ( x ( F |` { x } ) y -> z ( F |` { x } ) y ) )
5	4	moimdv	|- ( z = x -> ( E* y z ( F |` { x } ) y -> E* y x ( F |` { x } ) y ) )
6	5	spimvw	|- ( A. z E* y z ( F |` { x } ) y -> E* y x ( F |` { x } ) y )
7		vsnid	|- x e. { x }
8		vex	|- y e. _V
9	8	brresi	|- ( x ( F |` { x } ) y <-> ( x e. { x } /\ x F y ) )
10	7 9	mpbiran	|- ( x ( F |` { x } ) y <-> x F y )
11	10	biimpri	|- ( x F y -> x ( F |` { x } ) y )
12	11	moimi	|- ( E* y x ( F |` { x } ) y -> E* y x F y )
13	6 12	syl	|- ( A. z E* y z ( F |` { x } ) y -> E* y x F y )
14	1 13	simplbiim	|- ( Fun ( F |` { x } ) -> E* y x F y )