Theorem 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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		fnsnr	⊢ ( 𝐹 Fn { 𝐴 } → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
2	1	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
3		fnfun	⊢ ( 𝐹 Fn { 𝐴 } → Fun 𝐹 )
4		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
5	4	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐴 ∈ { 𝐴 } )
6		fndm	⊢ ( 𝐹 Fn { 𝐴 } → dom 𝐹 = { 𝐴 } )
7	6	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → dom 𝐹 = { 𝐴 } )
8	5 7	eleqtrrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐴 ∈ dom 𝐹 )
9		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
10	3 8 9	syl2an2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
11		eleq1	⊢ ( 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ → ( 𝑥 ∈ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
12	10 11	syl5ibrcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ → 𝑥 ∈ 𝐹 ) )
13	2 12	impbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
14		velsn	⊢ ( 𝑥 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ↔ 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
15	13 14	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
16	15	eqrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn { 𝐴 } ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
17	16	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
18		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
19		fnsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } )
20	18 19	mpan2	⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } )
21		fneq1	⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 Fn { 𝐴 } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } ) )
22	20 21	syl5ibrcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → 𝐹 Fn { 𝐴 } ) )
23	17 22	impbid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )