Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | fofn | $${\u22a2}{F}:{A}\underset{onto}{\u27f6}{B}\to {F}Fn{A}$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof | $${\u22a2}{F}:{A}\underset{onto}{\u27f6}{B}\to {F}:{A}\u27f6{B}$$ | |
2 | 1 | ffnd | $${\u22a2}{F}:{A}\underset{onto}{\u27f6}{B}\to {F}Fn{A}$$ |