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	⊢ 𝐴 ∈ V
Assertion	fnsnb	⊢ ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		fnsnb.1	⊢ 𝐴 ∈ V
2		fnsnr	⊢ ( 𝐹 Fn { 𝐴 } → ( 𝑥 ∈ 𝐹 → 𝑥 = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ) )
3		df-fn	⊢ ( 𝐹 Fn { 𝐴 } ↔ ( Fun 𝐹 ∧ dom 𝐹 = { 𝐴 } ) )
4	1	snid	⊢ 𝐴 ∈ { 𝐴 }
5		eleq2	⊢ ( dom 𝐹 = { 𝐴 } → ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ { 𝐴 } ) )
6	4 5	mpbiri	⊢ ( dom 𝐹 = { 𝐴 } → 𝐴 ∈ dom 𝐹 )
7	6	anim2i	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 = { 𝐴 } ) → ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) )
8	3 7	sylbi	⊢ ( 𝐹 Fn { 𝐴 } → ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) )
9		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
10	8 9	syl	⊢ ( 𝐹 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		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
18	1 17	fnsn	⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 }
19		fneq1	⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 Fn { 𝐴 } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } Fn { 𝐴 } ) )
20	18 19	mpbiri	⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → 𝐹 Fn { 𝐴 } )
21	16 20	impbii	⊢ ( 𝐹 Fn { 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )