Theorem funcnvs1

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

	Ref	Expression
Assertion	funcnvs1	$$⊢\mathrm{Fun}{⟨“A”⟩}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	$$⊢\mathrm{Fun}{\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}}^{-1}$$
2		df-s1	$$⊢⟨“A”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
3	2	cnveqi	$$⊢{⟨“A”⟩}^{-1}={\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}}^{-1}$$
4	3	funeqi	$$⊢\mathrm{Fun}{⟨“A”⟩}^{-1}\leftrightarrow \mathrm{Fun}{\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}}^{-1}$$
5	1 4	mpbir	$$⊢\mathrm{Fun}{⟨“A”⟩}^{-1}$$