Theorem funcrn | index | src |

theorem funcrn (A B F: set): $ func F A B -> Ran F C_ B $;
StepHypRefExpression
1 anr
isfun F /\ Dom F == A /\ Ran F C_ B -> Ran F C_ B
2 1 conv func
func F A B -> Ran F C_ B

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)