Theorem fnsnr

Description: If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when A is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016)

	Ref	Expression
Assertion	fnsnr	|- ( F Fn { A } -> ( B e. F -> B = <. A , ( F ` A ) >. ) )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	|- ( F Fn { A } -> ( F |` { A } ) = F )
2		fnfun	|- ( F Fn { A } -> Fun F )
3		funressn	|- ( Fun F -> ( F |` { A } ) C_ { <. A , ( F ` A ) >. } )
4	2 3	syl	|- ( F Fn { A } -> ( F |` { A } ) C_ { <. A , ( F ` A ) >. } )
5	1 4	eqsstrrd	|- ( F Fn { A } -> F C_ { <. A , ( F ` A ) >. } )
6	5	sseld	|- ( F Fn { A } -> ( B e. F -> B e. { <. A , ( F ` A ) >. } ) )
7		elsni	|- ( B e. { <. A , ( F ` A ) >. } -> B = <. A , ( F ` A ) >. )
8	6 7	syl6	|- ( F Fn { A } -> ( B e. F -> B = <. A , ( F ` A ) >. ) )