Theorem cicfval

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

	Ref	Expression
Assertion	cicfval	|- ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )

Proof

Step	Hyp	Ref	Expression
1		df-cic	|- ~=c = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )
2		fveq2	|- ( c = C -> ( Iso ` c ) = ( Iso ` C ) )
3	2	oveq1d	|- ( c = C -> ( ( Iso ` c ) supp (/) ) = ( ( Iso ` C ) supp (/) ) )
4		id	|- ( C e. Cat -> C e. Cat )
5		ovexd	|- ( C e. Cat -> ( ( Iso ` C ) supp (/) ) e. _V )
6	1 3 4 5	fvmptd3	|- ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )