Metamath Proof Explorer


Theorem elsetchom

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

Ref Expression
Hypotheses setcbas.c C=SetCatU
setcbas.u φUV
setchomfval.h H=HomC
setchom.x φXU
setchom.y φYU
Assertion elsetchom φFXHYF:XY

Proof

Step Hyp Ref Expression
1 setcbas.c C=SetCatU
2 setcbas.u φUV
3 setchomfval.h H=HomC
4 setchom.x φXU
5 setchom.y φYU
6 1 2 3 4 5 setchom φXHY=YX
7 6 eleq2d φFXHYFYX
8 5 4 elmapd φFYXF:XY
9 7 8 bitrd φFXHYF:XY