Theorem funcnvs1

Description: The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021)

	Ref	Expression
Assertion	funcnvs1	⊢ Fun ◡ ⟨“ 𝐴 ”⟩

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	⊢ Fun ◡ { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
2		df-s1	⊢ ⟨“ 𝐴 ”⟩ = { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
3	2	cnveqi	⊢ ◡ ⟨“ 𝐴 ”⟩ = ◡ { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ }
4	3	funeqi	⊢ ( Fun ◡ ⟨“ 𝐴 ”⟩ ↔ Fun ◡ { ⟨ 0 , ( I ‘ 𝐴 ) ⟩ } )
5	1 4	mpbir	⊢ Fun ◡ ⟨“ 𝐴 ”⟩