Theorem funcdm | index | src |

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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)