cicfval

Description: The set of isomorphic objects of the category c . (Contributed by AV, 4-Apr-2020)

		Ref	Expression
	Assertion	cicfval	$⊢ C \in Cat \to ≃_{𝑐} (C) = Iso (C) supp \emptyset$

Step	Hyp	Ref	Expression
1		df-cic	$⊢ ≃_{𝑐} = (c \in Cat ⟼ Iso (c) supp \emptyset)$
2		fveq2	$⊢ c = C \to Iso (c) = Iso (C)$
3	2	oveq1d	$⊢ c = C \to Iso (c) supp \emptyset = Iso (C) supp \emptyset$
4		id	$⊢ C \in Cat \to C \in Cat$
5		ovexd	$⊢ C \in Cat \to Iso (C) supp \emptyset \in V$
6	1 3 4 5	fvmptd3	$⊢ C \in Cat \to ≃_{𝑐} (C) = Iso (C) supp \emptyset$

Metamath Proof Explorer