Theorem fnsnb

Description: A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) Revised to add reverse implication. (Revised by NM, 29-Dec-2018)

	Ref	Expression
Hypothesis	fnsnb.1	|- A e. _V
Assertion	fnsnb	|- ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } )

Proof

Step	Hyp	Ref	Expression
1		fnsnb.1	|- A e. _V
2		fnsnr	|- ( F Fn { A } -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
3		df-fn	|- ( F Fn { A } <-> ( Fun F /\ dom F = { A } ) )
4	1	snid	|- A e. { A }
5		eleq2	|- ( dom F = { A } -> ( A e. dom F <-> A e. { A } ) )
6	4 5	mpbiri	|- ( dom F = { A } -> A e. dom F )
7	6	anim2i	|- ( ( Fun F /\ dom F = { A } ) -> ( Fun F /\ A e. dom F ) )
8	3 7	sylbi	|- ( F Fn { A } -> ( Fun F /\ A e. dom F ) )
9		funfvop	|- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
10	8 9	syl	|- ( F Fn { A } -> <. A , ( F ` A ) >. e. F )
11		eleq1	|- ( x = <. A , ( F ` A ) >. -> ( x e. F <-> <. A , ( F ` A ) >. e. F ) )
12	10 11	syl5ibrcom	|- ( F Fn { A } -> ( x = <. A , ( F ` A ) >. -> x e. F ) )
13	2 12	impbid	|- ( F Fn { A } -> ( x e. F <-> x = <. A , ( F ` A ) >. ) )
14		velsn	|- ( x e. { <. A , ( F ` A ) >. } <-> x = <. A , ( F ` A ) >. )
15	13 14	bitr4di	|- ( F Fn { A } -> ( x e. F <-> x e. { <. A , ( F ` A ) >. } ) )
16	15	eqrdv	|- ( F Fn { A } -> F = { <. A , ( F ` A ) >. } )
17		fvex	|- ( F ` A ) e. _V
18	1 17	fnsn	|- { <. A , ( F ` A ) >. } Fn { A }
19		fneq1	|- ( F = { <. A , ( F ` A ) >. } -> ( F Fn { A } <-> { <. A , ( F ` A ) >. } Fn { A } ) )
20	18 19	mpbiri	|- ( F = { <. A , ( F ` A ) >. } -> F Fn { A } )
21	16 20	impbii	|- ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } )