This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcnvs1

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

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

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