Theorem funressneu

Description: There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu . A e. _V is required because otherwise E! y A F y , see brprcneu . (Contributed by AV, 7-Sep-2022)

	Ref	Expression
Assertion	funressneu	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> E! y A F y )

Proof

Step	Hyp	Ref	Expression
1		simp1l	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> A e. V )
2		simp1r	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> B e. W )
3		simp3	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> A F B )
4		breldmg	|- ( ( A e. V /\ B e. W /\ A F B ) -> A e. dom F )
5	1 2 3 4	syl3anc	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> A e. dom F )
6		eldmg	|- ( A e. dom F -> ( A e. dom F <-> E. y A F y ) )
7	6	ibi	|- ( A e. dom F -> E. y A F y )
8	5 7	syl	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> E. y A F y )
9		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
10	9	anim1i	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) ) -> ( A e. V /\ Fun ( F |` { A } ) ) )
11	10	3adant3	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> ( A e. V /\ Fun ( F |` { A } ) ) )
12		funressnmo	|- ( ( A e. V /\ Fun ( F |` { A } ) ) -> E* y A F y )
13	11 12	syl	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> E* y A F y )
14		moeu	|- ( E* y A F y <-> ( E. y A F y -> E! y A F y ) )
15	13 14	sylib	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> ( E. y A F y -> E! y A F y ) )
16	8 15	mpd	|- ( ( ( A e. V /\ B e. W ) /\ Fun ( F |` { A } ) /\ A F B ) -> E! y A F y )