Theorem elsetchom

Description: A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcbas.c	|- C = ( SetCat ` U )
	setcbas.u	|- ( ph -> U e. V )
	setchomfval.h	|- H = ( Hom ` C )
	setchom.x	|- ( ph -> X e. U )
	setchom.y	|- ( ph -> Y e. U )
Assertion	elsetchom	|- ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )

Proof

Step	Hyp	Ref	Expression
1		setcbas.c	|- C = ( SetCat ` U )
2		setcbas.u	|- ( ph -> U e. V )
3		setchomfval.h	|- H = ( Hom ` C )
4		setchom.x	|- ( ph -> X e. U )
5		setchom.y	|- ( ph -> Y e. U )
6	1 2 3 4 5	setchom	|- ( ph -> ( X H Y ) = ( Y ^m X ) )
7	6	eleq2d	|- ( ph -> ( F e. ( X H Y ) <-> F e. ( Y ^m X ) ) )
8	5 4	elmapd	|- ( ph -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
9	7 8	bitrd	|- ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )