fnsnbg

Description: A function's domain is a singleton iff the function is a singleton. (Contributed by Steven Nguyen, 18-Aug-2023) Relax condition for being in the universal class. (Revised by Zhi Wang, 21-Oct-2025)

		Ref	Expression
	Assertion	fnsnbg	\|- ( A e. V -> ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } ) )

Proof

Step	Hyp	Ref	Expression
1		fnsnr	\|- ( F Fn { A } -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
2	1	adantl	\|- ( ( A e. V /\ F Fn { A } ) -> ( x e. F -> x = <. A , ( F ` A ) >. ) )
3		fnfun	\|- ( F Fn { A } -> Fun F )
4		snidg	\|- ( A e. V -> A e. { A } )
5	4	adantr	\|- ( ( A e. V /\ F Fn { A } ) -> A e. { A } )
6		fndm	\|- ( F Fn { A } -> dom F = { A } )
7	6	adantl	\|- ( ( A e. V /\ F Fn { A } ) -> dom F = { A } )
8	5 7	eleqtrrd	\|- ( ( A e. V /\ F Fn { A } ) -> A e. dom F )
9		funfvop	\|- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
10	3 8 9	syl2an2	\|- ( ( A e. V /\ 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	\|- ( ( A e. V /\ F Fn { A } ) -> ( x = <. A , ( F ` A ) >. -> x e. F ) )
13	2 12	impbid	\|- ( ( A e. V /\ 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	\|- ( ( A e. V /\ F Fn { A } ) -> ( x e. F <-> x e. { <. A , ( F ` A ) >. } ) )
16	15	eqrdv	\|- ( ( A e. V /\ F Fn { A } ) -> F = { <. A , ( F ` A ) >. } )
17	16	ex	\|- ( A e. V -> ( F Fn { A } -> F = { <. A , ( F ` A ) >. } ) )
18		fvex	\|- ( F ` A ) e. _V
19		fnsng	\|- ( ( A e. V /\ ( F ` A ) e. _V ) -> { <. A , ( F ` A ) >. } Fn { A } )
20	18 19	mpan2	\|- ( A e. V -> { <. A , ( F ` A ) >. } Fn { A } )
21		fneq1	\|- ( F = { <. A , ( F ` A ) >. } -> ( F Fn { A } <-> { <. A , ( F ` A ) >. } Fn { A } ) )
22	20 21	syl5ibrcom	\|- ( A e. V -> ( F = { <. A , ( F ` A ) >. } -> F Fn { A } ) )
23	17 22	impbid	\|- ( A e. V -> ( F Fn { A } <-> F = { <. A , ( F ` A ) >. } ) )

Metamath Proof Explorer

Theorem fnsnbg

Proof